WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s - #1010
Draft
MauroToscano wants to merge 1168 commits into
Draft
MauroToscano wants to merge 1168 commits into
MauroToscano wants to merge 1168 commits into
Conversation
…ed FriFoldLayout New `fri::schedule`: the integer dynamic program of FRI.md §2.1 that picks the fold exponent of each committed FRI layer from public shape constants only (first committed size, terminal size, query count, the cap-height function as a parameter, DMAX = 6). Cost is kept in units of 1/Q so the format function is u64-only, with the (cost, trees) lexicographic tie rule (smallest d first). Also the FriMode / OneRowMode enums and FriFormat, the verifier-side constants a layout is built from. `FriFoldLayout` gains `schedule` (per committed layer) and `one_row`; `num_committed = schedule.len()`. `FriFoldLayout::new` is now `for_format(.., FriFormat::LEGACY)`, i.e. the all-ones schedule through the general constructor, and produces the same total_folds / num_committed / terminal_len / effective_k as before. The struct is no longer Copy (it owns a Vec); no call site copied it. No caller uses a non-legacy format yet, so no behaviour changes; ProofOptions and every serialized type are untouched. Tests (fri_schedule_tests): the FRI.md §2.2 table pinned for T = 9 and 10 under three cap functions (off, the design model's, CAP.md §2 Auto, implemented locally until the cap primitive lands); brute-force optimality of the DP for b0 <= 16; legacy_layout_equals_old_layout against a verbatim copy of the old constructor over B <= 30, blowup_log 1..4, k 0..10.
…fold word
WhirFolds becomes { Uniform, First(FirstFold) }: the first round folds k0
variables (all of them when the chain has fewer) and every later round is
today's walk, log_folding with the remainder last. A config serves chains of
every height, so a per-round list would have to say what a shorter chain
does with it; the lever design/WHIR.md measured is the first fold alone.
The C2 skeleton's Dp and List variants are removed (RULINGS 15: no DP, and
the knob is uniform4 | first5 | first6). FirstFold holds 1..=MAX_FOLD (6),
the widest fold the stack is tested at; nothing else is constructible.
- schedule(): Uniform runs today's body verbatim (tested against a copy of
it for n <= 40, k 1..=6).
- with_security_folds(): Q is charged the worst round count of any chain of
<= tallest variables under the schedule. Uniform gives exactly today's
config (tested on the grid); first5/first6 never add a round at any height,
so Q never rises, and it is 112 at 25 (6 rounds instead of 7).
- fold_word(): the statement word. Uniform = log_folding (4u64 at the
default, today's bytes); First(k0) = 1<<63 | log_folding<<52 | 1<<48 | k0
(design/WHIR.md's prefix encoding, one entry). Not absorbed yet.
- zf_format: LAMBDA_VM_ZF_WHIR_FOLDS accepts uniform4 | first5 | first6 and
refuses dp, lists and other first<k>. WHIR_FOLDS_IMPLEMENTED stays false.
Host prove/verify at k0 = 5, 6 (n = 3..11), a tampered 64-wide base block
rejected, and a first6 proof refused under uniform4 (and back).
S5: CapPolicy::Auto is now RULINGS 1's table stated directly (3 from 20 openings, 2 from 4, else 0, clamped to the depth), with the thresholds as named format constants. No arithmetic runs on the policy path, so no verifier can disagree on an overflow. cap_gain stays (the FRI schedule DP prices with the same weights) but is bounded: a height past MAX_CAP_HEIGHT returns i128::MIN instead of shifting, and every term fits i128 for any usize opening count, on 32-bit wasm too. Pinned: the table is the cost-law argmax for every opening count up to 10^6 and at the usize extremes. The depth-clamped table and a depth-bounded argmax differ at exactly one point (4 openings, depth 1: table 1, argmax 0); a test pins that single difference. M1: two fixtures that only one check rejects, on the real keccak backend: - the real internal node above leaf 0 / leaf 2^D-1 presented as a leaf hash with a path one sibling short: the length-agnostic fold accepts it, only siblings.len() == D - c rejects it (every c < D, c = 0 is C1b); - an unreached cap node flipped with 3 queries at c = 3: every per-query check passes, only the cap-to-root check rejects it. Checked by hand: deleting the length check or the verify_cap call in from_owner makes the matching test fail.
…itments agree on it The three host absorbs (monolithic, epoch, global) and the LFM emitter's push_config write ChainConfig::fold_word() where they wrote log_folding. At the default schedule that is log_folding itself, 4u64, so every default statement, transcript KAT and byte gate keeps its bytes; under first5/first6 it is a tagged word, so the 245-byte statement keeps its length and moves in those 8 bytes only. The schedule of every chain is f(word, num_vars) and the heights are already bound, so the word binds every schedule, including the heights (num_vars <= 4) where first6 and uniform4 give the same schedule and the same Q and only the word tells two proofs apart. agrees_with (DecodePrepared, GenesisPrepared, GlobalPrepared) now compares (log_blowup, log_folding, folds): commit_stacked blocks tree 0 at the schedule's first fold, so a first6 commitment has 64-wide leaves that a uniform4 epoch would open as 16-wide ones. One helper, committed_under, makes the comparison for all three. Tests: a_first_fold_statement_moves_only_its_fold_word (length kept, only the fold word moves, the machine draws the host's challenge under first5 and first6); the_fold_word_alone_separates_two_schedules_that_agree (mutation gate: two configs equal in every field and schedule but the policy draw different challenges at all three host sites; with fold_word() forced to log_folding it and the test above FAIL, checked by hand); a_decode_commitment_refuses_another_fold_schedule.
chain_config now builds through chain_config_under(format, shapes), which calls ChainConfig::with_security_folds with the format's fold schedule, so Q is charged the schedule's own worst round count rather than the uniform one with the format stamped on afterwards. At the default this is exactly the previous config (tested: chain_config_under(DEFAULT) == chain_config); under first5/first6 Q stays 112 at the block's tallest stack (25), with 6 rounds instead of 7. decode_prepared_config and the five continuation call sites go through chain_config and inherit the schedule. ZfFormat::global() prints a second line under the banner, on every setting: "ZF WHIR SCHEDULES: whir_folds=… q=… n=20:[…] … n=25:[…]", the schedules the base chains run at the production heights, so a log states the rounds it proved and not only the knob's name. WHIR_FOLDS_IMPLEMENTED stays false until the GPU and in-guest gates land.
…ut, schedule override RULINGS 13 / REVIEW-FRI F2: the fold-schedule DP now minimises the same cost-law objective as the cap policy, per query per committed layer: leaf blocks and walk levels priced with the cap policy's AUTO_WEIGHTS (compress, select), minus the tree's cap gain; plus the slot mux (2^d - 1 selects), the group fold (2^d - 1 binary folds at 5 XALU rows, edsl::fri_fold) and the twiddle chain (d BALU muls). XALU and BALU rows are priced from the node cost law at their committed widths (18 and 10 cells: 522 and 477 ns). FRI_COST_WEIGHTS is a format constant, pinned. The generic DP (fri_schedule_by) keeps the design model's permutation objective as a second instance, still pinned against the FRI.md 2.2 table, so the DP machinery stays checked against an independent model. U1 is re-pinned from the Rust DP (T = 9 and 10, B = 6..24, cap Off and Auto, S3 and S2 chains); at T = 9 under Auto it matches REVIEW-FRI F2's independent cost-law column at every B it lists. U2 brute-forces the new objective (4 cap policies x 3 query counts x 4 dmax, b0 <= 16). RULINGS 18: FriMode / OneRowMode now come from stark::proof::options (the local enums are gone); the cap input is a CapPolicy, and the test- local Auto cap is CapPolicy::Auto.height. FriFoldLayout::for_options builds the layout from ProofOptions (the format is a verifier-side constant) and records the encoding: legacy (pair leaves, one sibling per layer) exactly for fri=pair with row-pair openings, decided by the format, not the schedule's values. A one-row mode other than Off is an error (S2 is not built), never a silent row-pair proof. REVIEW-FRI F1.3: ProofFormat.fri_schedule_override, a test hook that replaces the DP's schedule under fri=dp so round trips can use schedules the DP never picks. No knob sets it (ZfFormat leaves it None); a schedule that does not cover the table's folds is an error; is_default() requires it None. ProofFormat is not serialized (skipped by serde and rkyv), so no pinned byte moves. No prover or verifier path uses the new layout yet; defaults unchanged.
W2's first6 schedule folds 6 variables in round 0, so tree 0's leaves are 64 base felts and the first fold runs six levels in one residency. GPU parity covered k <= 5. - whir_commit every_shape (both hashes): parity at (14, 2, 6), (12, 2, 6) and (7, 1, 6) (four leaves). Root, codeword, and openings against the host pipeline, through commit_codeword_to_host, which has no host fallback. - whir_fold: the_device_folds_six_levels_as_the_host_does, six levels on the base codeword at 2^16, 2^14 and 2^8, against fold_codeword_k_on_host. It calls math_cuda::whir::fold_codeword_base directly, because whir::fold_codeword_k falls back to the host silently (size threshold, kill switch) and a comparison through it can be the host against itself. Box only: the laptop has no CUDA (clippy with stub cubins is green).
…ifier (W1, C6)
Every WHIR commitment tree can now be opened under a Merkle cap: each
authentication path stops c levels below the root, and the tree's cap
(its 2^c nodes at that height) rides once, at the end of the tree's
first opening in proof order (the owner-path encoding, design/CAP.md
section 3). No struct changes, nothing new absorbed: the root is still the
commitment. At the default (CapPolicy::Off) every height is 0 and the
proof bytes are today's.
- ChainConfig::tree_caps: one height per tree from config.format.cap,
CapPolicy::height(openings, depth) with depth = D_t - k_t and openings Q
for tree 0, 2Q for every later tree (the last included). Shared by the
prover, the host verifier and (next commit) the LFM ChainShape.
- CodewordCommitment::open_many_capped(indices, c, owner): paths cut to
depth - c, the owner's first path carrying the cap. Host trees read
MerkleTree::cap; device codewords read the cap in the SAME with_tree
rebuild as the paths (DeviceCodeword::paths_and_cap, math-cuda + the
multilinear gpu.rs wrapper), so the cap costs no extra tree build and
retention/eviction are untouched. open_many is open_many_capped(.., 0, _).
- whir_round::prove takes RoundCaps; round 0 owns tree 0, every round owns
its successor. final_openings likewise (a one-round chain's tree 0 is
owned by the final openings).
- Verifier: TreeCheck { Owner, Checked }. A tree is authenticated ONCE,
by CappedRoot::from_owner on its owner opening; round t opens tree t
against the check round t-1 returned and never re-reads a cap (a cap on
round t's first current opening fails its exact length). The checks are
built after the opening-count guards, from .first(), so a short proof is
refused, never a panic (REVIEW-CAP M2).
- Default-path hardening, the WHIR analogue of C1b (RULINGS 3/16):
whir_commit::verify_opening now takes the tree depth and requires an
exact-length path (CappedRoot::uncapped). Honest proofs are unaffected;
only malformed proofs see a difference. New verify_opening_capped.
- New errors: CapRejected (verifier), CapEmbedFailed (prover).
Tests (laptop, multilinear --lib whir_*): capped chains round-trip at
Fixed(1..3) and Auto, Q 3 and 25, one-round, multi-round, remainder,
base and extension rounds, keccak and RPX, with every path length pinned
(depth - c, owner + 2^c); Off and Fixed(0) give identical rkyv bytes;
transcript invariance Off vs Fixed(3)/Auto (REVIEW-CAP S2); tamper arm
(tree-0 cap, tree-t cap in rounds[t-1].next[0], a second cap on round t's
current[0], owner path +-1, non-owner path +-1, cap moved to query 1, a
sibling, a proof read under another policy); M1(b) an unreached cap node
that every per-query check accepts, refused as CapRejected only by the
cap-to-root check (both trees of a round); M1(a) a keccak leaf forged
from an internal node (8 base values = 64 bytes = a parent input) that
the raw fold accepts, refused by the exact length alone; M2 an empty
capped round refused without a panic; tree_caps pinned at production
(Auto [3,3,3,3,3,3,2]).
No emitter change: ChainShape builds from config.schedule, so the closed forms, the arena layout, the query phase and the slot mux follow the schedule. What was missing is gates at k = 5 and 6. - whir_fold_tests SHAPES gain (12, 5, 7) and (13, 6, 7): blocks of 32 and 64, closed form, interned constants by value, and the fold against the host over extension and base blocks. - whir_chain_tests: KNOB_COST_SHAPES (S = 9 first6 [6,3], S = 11 first5 [5,4,2] at grind 0 and 8; S = 6 [6] and S = 7 [6,1] under first6) join the schedule gate (the emitter's hash schedule is the host transcript's) and the closed-form gate, through a cost_configs() list that keeps COST_SHAPES at the default schedule. A first-fold chain executes on a proof the host accepts; the tamper arm refuses the last value of a 64-wide base block, a round-0 sibling and the successor block, each rejected by the host too. - Knob-on production pins at S = 25, Q = 112, grind 20, derived by hand (parents, leaf blocks) and equal to design/WHIR.md's independent model: first6 19,600 opening / 19,877 chain permutations / 201,318 rows; first5 20,832 / 21,109 / 189,028. The ignored F1 at the production shape emits both programs and matches (run on the laptop: 0.08 s, 153 MB). - PREPARED_LEG_ROWS stays fixed (RULINGS 15); a knob-on test asserts it still covers the 20-variable stack: 137,321 rows under first5, 155,889 under first6, against 175,066. Default pins unchanged (22,512 / 22,828 / 185,509 and the band test).
Every tree of a univariate STARK proof (main, precomputed, aux, composition and each committed FRI layer) now honours ProofOptions.format.merkle_cap. - merkle_caps.rs (new): StarkCaps, the one place the heights are computed from public shape (policy, query count, log2(lde), committed layer count; trace trees log2(lde)-1 deep, FRI layer i log2(lde)-i-2); TreeCheck, the verifier's per-tree check (built once, then used for every query); TableTreeChecks. - Prover: a post-pass in round 4 after the openings. Per capped tree it reads the cap from the host tree and embeds it on the owner path (query 0), cutting every path to D - c. Round 4 now returns a Result. A device-resident tree (root-only host tree) is a hard DevicePath error that names the tree until the device read lands (REVIEW-CAP S6); a host tree whose depth is not the format's is refused. - Verifier: table_tree_checks builds every tree's check once, after the query-count and opening-width guards and with length-checked access only, so a malformed proof rejects and never panics (REVIEW-CAP M2). At c = 0 it reads no opening at all and is exactly the C1b exact-length check. Every opening (trace, precomputed, aux, composition, FRI layer) goes through its tree's check with its query position; query 0 of a capped tree uses the owner siblings split off once. Nothing is absorbed, so the transcript is unchanged, and at the default every height is 0: no path is cut, no cap is appended, the bytes are the same. MERKLE_CAP_IMPLEMENTED stays false until the device arm (C4) is in. Tests (tests::merkle_cap_tests, small AIRs, laptop): - round trips at Fixed(1..=4) and Auto, 3/8/30 queries, blowup 2 and 4, owned and archived (rkyv, multi_verify_archived), with the path shapes pinned (owner D-c+2^c, others D-c, the cap hashes to the root); - a preprocessed table and a RAP (aux) table capped, every cap node bound; - Off == Fixed(0) == Auto-at-3-queries, byte for byte; - REVIEW-CAP S2: Off vs Auto at grinding 0 give equal roots, OOD values, final coefficients, nonce and opened values; only paths differ, each the full path cut to D - c (+ the cap on the owner); - tampers: every cap node of main/composition/first and last FRI layer, every node of a later query's path, the owner one node short/long, the cap on a non-owner, the cap moved to query 1, and a proof made under one policy verified under another (both directions); - REVIEW-CAP M1 at the verifier level: an unreached cap node (3 queries, c = 3) that only the cap-to-root check rejects, and the real internal node above a queried leaf passed as a leaf hash, which the verifier's own TreeCheck refuses and the length-agnostic fold accepts. Deleting verify_cap or the length check from the primitive fails both (checked by hand); - S6: a root-only tree with no device read is an Err naming the tree.
…1, C7) The device side of W1 landed with the host commit (the Codeword::Device arm of open_many_capped must compile): DeviceCodeword::paths_and_cap reads the cap as the heap slice [2^c - 1, 2^(c+1) - 1) of the node buffer the paths are gathered from, inside ONE with_tree rebuild. These are its box gates; the laptop has no CUDA, so they only compile here. - math-cuda/tests/whir_cap.rs: for k = 1..5 under keccak and RPX, every cap height up to min(depth, 6): the device paths equal the host tree's full paths, the height-0 cap is the root, and the device cap equals the cap the host owner encoding appends. In three leaf-layer regimes: served from the retained layer (0 extra leaf passes), rehashed at another blocking (1), and after the allocator's evictor reclaimed the layer. Each call is exactly one tree build (tree_builds + 1): the cap costs no extra rebuild. - multilinear/tests/whir_cap_device.rs (cuda-gated): a 2^16-variable chain whose codeword stays on the card (asserted) proves the same rkyv bytes as the chain over a host-held codeword at Off, Auto and Fixed(5), both hashes, and the host verifier accepts it; tree 0's owner path length is pinned.
LAMBDA_VM_ZF_WHIR_FOLDS=first5 | first6 is now selectable: host chain, statement word, agrees_with, the production config, the GPU parity cases at k = 6 and the in-guest gates at k = 5 and 6 are in. The GPU parity tests run on the box (no CUDA on the laptop); the knob-on block proofs are the box request that follows.
REVIEW-FRI F1: nothing proved the default FRI format byte-identical. A round trip cannot (a drifted prover accepts its own proofs), and proof bytes are not reproducible under grinding (parallel nonce search). These goldens prove at grinding_factor = 0, where the bytes ARE reproducible (checked: two runs, identical), and pin, per case, the digest of the proof's rkyv bytes plus separately its FRI layer roots, terminal coefficients, FRI decommitments and trace/composition openings, so a failure names the field that drifted. Generated before any S3 prover code, on the schedule-DP commits (which change no prover path): - stark::tests::zf_golden_tests (SHA3-256): Keccak and Blake3; SimpleAddition (E = F) and LogReadOnlyRAP (E = F^3, aux); blowup 2 and 4; total_folds 0, 1, 2, 3, 4, 6; one CPU/ADD/MUL multi_prove bus proof. - prover tests::zf_rpx_golden_tests (SHA-256): the same AIRs under the production RPX pin (RpxStarkHash), which the stark crate cannot name. Shown able to fail: swapping the pair order of the FRI layer leaves in the CPU prover turns default_format_goldens_are_byte_identical red. sha3 becomes a stark dev-dependency (the version crypto already links).
…ippy) assertions_on_constants: WHIR_FOLDS_IMPLEMENTED is a const, so the check is a const block. make fmt and make lint green.
The R4 cap post-pass now reads a device-resident tree's cap instead of
refusing it: math_cuda::merkle::read_cap_dev is one D2H of the heap slice
[(2^c-1)*32, (2^{c+1}-1)*32) (the device heap has the host layout, so these
are the nodes MerkleTree::cap returns), and gpu_lde::read_cap_dev wraps it
with shape checks that fail closed with a message, never a panic. The
device arms: main and aux (gpu_main/gpu_aux trees, the table's bound
stream), composition (gpu_composition_tree) and each FRI layer (gpu_tree, a
fresh backend stream as the device FRI query phase uses). The precomputed
tree is always a full host tree. No kernel, no commit-phase change: paths
are still gathered in full and cut on the host (the merkle_gather parity is
untouched). New counter gpu_cap_read_calls.
MERKLE_CAP_IMPLEMENTED is now true (C3 + C4 are both in), so
LAMBDA_VM_ZF_CAP no longer aborts. The in-guest LFM verifier (C5) does not
verify caps yet: a recursion run that wraps a capped proof fails there, so
the knob is for STARK-level tests until C5.
Tests (box only; the laptop has no CUDA, cuda clippy is the laptop gate):
- math-cuda tests/merkle_cap.rs: keccak trees 2^1..2^8, 2^12, 2^18, 2^22
leaves, every c <= min(D, 6): the device read equals the host cap and the
heap slice, c = 0 the root; RPX trees equal the device's own heap slice;
a kept composition tree (GpuMerkleTree) serves its cap and root;
- stark tests::merkle_cap_tests::device_trees_serve_their_caps (ignored,
cuda): a 2^14-row cubic LogUp table proved at Auto/30 queries takes caps
off the device (counter moves), verifies owned and archived, and matches
an Off proof of the same witness with every path cut to D - c;
- zf_format::the_merkle_cap_knob_is_selectable.
prover/tests/merkle_cap_vm.rs proves an ELF through prove_with_options_and_inputs with the options the process format names (ZfFormat::from_env, so LAMBDA_VM_ZF_CAP), verifies it under the same options, and checks the default-format verifier refuses it (Ok(false) or Err, never a panic or an accept). Every production table is capped: preprocessed precomputed + main trees, LogUp aux trees, composition trees, FRI layers. CPU fixture all_instructions_64; under cuda fib_iterative_1M, whose tables commit on the device, and the caps must come off the resident trees (gpu_cap_read_calls moves). Knob-on only: #[ignore], and it refuses to run with the cap off. Box only (it proves a real trace).
… cost model (W1, C8)
The level-0 WHIR wrap now verifies capped chains (design/CAP.md 6.2).
Everything is derived from ChainShape.caps = ChainConfig::tree_caps, the
same heights the host prover and verifier use; at the default every
height is 0 and the emitted program, the arena and every pin are today's
(no new arena, no new word, the root path instruction for instruction).
- whir_open: CapCells, whose only constructor authenticate() hashes the
hinted cap to its root (2^c - 1 compressions) and asserts it equals the
tree's root lanes, once per tree. TreeAuth { Root, Cap }: every opening
goes through TreeAuth::verify_opening with the WHOLE index; it walks the
low bits and a private mux (2^c - 1 Selects, pairs (2t, 2t+1), low bit
first) consumes exactly the top c, then compares two variable cells. So
the cap the mux reads is the cap the root check read (REVIEW-CAP (e)),
and no caller splits the index for the mux ((d), S1 in its WHIR form).
Closed forms: verify_opening_{rows,perms}_capped, cap_check_{rows,perms}.
- whir_chain: ChainShape.caps, current_path (the sibling count; current_depth
stays the index-bit count, the two meanings the map flagged). Tree 0's
cap is authenticated at the top of emit_verify_weighted, each successor's
where its root is unpacked, and carried to the next round with it.
Arena: tree 0's 2^c words right after round 0's nonces, tree r+1's right
after round r's successor root and ood value, paths depth - c
(round_words, RoundStorage::hint, push_round_words split the owner path).
Cost model: chain_opening_perms carries depth - c per opening plus
chain_cap_perms; chain_query_rows the capped opening rows; chain_fixed_rows
the per-tree cap checks. Hints stay arena words (the chain's plumbing).
Pins that move only with the knob on (all default pins unchanged):
production chain S=25 k=4 Q=112 grind=20 at Auto, caps [3,3,3,3,3,3,2]:
opening perms 22,512 -> 18,413 (-4,144 + 45), perms 22,828 -> 18,729,
shape rows 184,673 -> 187,245, rows 185,509 -> 188,081 (hand-derived in the
test doc, then run). Emitted at the production shape (ignored, laptop-safe):
188,081 rows / 18,729 perms == the forms; 37,968 Select (+5,152 a chain).
PREPARED_LEG_ROWS stays fixed (RULINGS 4): under Auto it is within 2% of
the 24-variable chain and still covers the 20-variable stack (tested).
Tests (laptop): capped chains execute on host-accepted proofs at Fixed(1),
Fixed(2), Auto, Q 3 and 25, one and three rounds; emitted rows and perms ==
the forms at Fixed(2), Fixed(3), Auto; the host transcript schedule is
unchanged under the cap; tamper: an UNREACHED tree-0 cap node (positions
from the host's own draws: only the cap-to-root check can refuse it), a
reached one, and a successor's cap node, each rejected by the host and with
no execution; the cap mux selects every index (all 64 leaves of a depth-6
tree, c = 1..3) and refuses the right leaf claimed in another subtree; an
unreached tampered cap word cannot execute; capped opening and cap check
closed forms at every height of a depth-6 tree.
…able WHIR_CAP_IMPLEMENTED flips to true now that the cap is in the host prover and verifier (C6), on the device (C7) and in the in-guest verifier and its cost model (C8). ZfFormat no longer aborts on LAMBDA_VM_ZF_WHIR_CAP=auto or a fixed height; the default (off) is unchanged. A zf_format test pins that the knob is selectable.
…verifier (H2)
Under LAMBDA_VM_ZF_FRI=dp (ProofFormat.fri_mode = Dp) committed FRI layer
j folds by 2^{d_j}, d_j from the verifier-side schedule DP (FRI.md 1-3,
with REVIEW-FRI F5/F6 applied). The legacy format (fri = pair) runs
today's code, byte for byte: the H0 goldens are unchanged.
Prover (fri/mod.rs): commit_phase_with_layout. Per committed layer:
sample zeta, fold d_{j-1} times with zeta, zeta^2, ... (d_{-1} = 1: fold
0 is the binary fold of the DEEP pair; F6's fold-count fix), commit the
result, append the root; the final zeta folds d_last times into the
terminal. The fold is the unchanged binary fold. Group trees hash each
2^d-value group with H::Batched and build parents with H::Pair, as
today's layer trees (built with Pair, verified with Batched).
query_phase_with_layout opens the full group (the query's own value
included, FRI.md 3.4) and the path of leaf p >> d. Proof structs are
unchanged: the flat layers_evaluations_sym carries every layer's group
under a non-legacy format (its length a verifier constant).
Verifier: fri_termination_params builds the layout from the AIR's
options (never the proof); a format it cannot lay out is rejected. The
group checks live in fri::group::verify_query_groups: per layer the
group is hashed in full and authenticated at the exact depth, the slot
check group[p & (2^d - 1)] == v, and the group fold (d binary levels on
the fiber, x_g^-1 from the query point and the slot). The structural
check pins the value count per query before any loop.
The legacy/group encoding is decided by the format, not the schedule's
values (F5's per-table predicate reduces to the format until S2).
Device: every device FRI arm (DEEP-to-FRI on device, the device commit,
the device query gather) runs only for the legacy encoding; a dp table
takes the CPU FRI loop (DEEP may still run on the device, its values are
format-independent). One-row modes are refused (Err), not proved.
Round 4 now returns Result: an unsupported format is a ProvingError.
Tests (tests::fri_group_tests, prover tests::zf_rpx_golden_tests):
- U4 group_fold_equals_d_binary_folds (d = 1..6, every group and slot,
and 2^d * sum zeta^i f_i from the polynomial);
- U5 group_leaf_is_a_coset (b <= 10);
- U6 round trips at dp: every fold count 0..9 at blowup 2 and 4; explicit
schedules [1,3,3] [3,1,3] [2,1,2,2] [1]*7 [6,1] [1,6] [4,3]; ext3 with
aux; a multi-table bus proof; Keccak, Blake3 and RPX; a non-covering
override is a proving error;
- the format is a verifier constant (dp proof rejected under pair and
vice versa);
- F1.2 generic_path_at_all_ones_equals_legacy (Keccak and RPX): same
roots, terminal, openings, paths; each group is the legacy pair;
- T1-T3: every group value of a query (slot and non-slot), a path
sibling, a root, values one short / long, a short path, a missing layer;
- M1 the slot check and M2 the group authentication are load-bearing:
a p0 + c FRI forgery / a foreign root is ACCEPTED with the check
switched off (test-only thread-local mutation) and rejected with it.
Shown able to fail: folding d_j instead of d_{j-1} (F6's bug) turns 8
S3 tests red while the goldens and the all-ones differential stay green.
FRI.md 10, "Vectors the host lane exports" (a)-(d), checked in under
crypto/stark/tests/vectors/zf_fri/ with a README (conventions: field and
limbs, bit-reversed coset layers, the binary and group folds, group-leaf
hashing, query/leaf/slot arithmetic, transcript, proof encoding):
(a) a_schedules.json: the DP's schedules and cost-law costs, T in
{4, 9, 10}, Q in {3, 110}, cap off/auto, B = 6..24, S3 and S2 chains;
(b) b_group_folds.json: a SplitMix64 KAT codeword (2^7 ext3 values, the
generator documented) folded d = 1..6 times; the generator asserts
the verifier's group fold of every group reproduces the prover's;
(c) c_leaf_digests_{keccak,blake3,rpx}.json: the first group's leaf
digest and the whole group-leaf layer root, d = 1..6;
(d) d_proof_{keccak,blake3,rpx}_{pair,dp,dp_3_1_3}.{rkyv,json}: a
LogReadOnlyRAP proof (B = 12, blowup 4, k = 2, Q = 3, grinding 0) per
format, with the layout, roots, every zeta, the terminal
coefficients, and per query iota, the DEEP pair and per layer the
position, leaf, slot, opened values and path length.
The generators live in stark::fri::vectors (test / test-utils only, so
the prover crate generates the RPX files with the same code). zeta,
iota and the DEEP values come from the host verifier itself, through a
test-only thread-local capture (stark::fri::capture). The tests
zf_fri_vectors::vectors_are_current (stark) and
tests::zf_rpx_vectors::rpx_vectors_are_current (prover) regenerate every
file in memory and require it byte-equal to the checked-in copy.
prover tests::zf_vm_dp_tests::a_vm_proof_round_trips_at_fri_dp: a real
multi-table VM proof (test_mul_8, the preprocessed tables included,
RPX, CPU FRI) proved and host-verified at fri = dp, rejected by the
default-format verifier and after a group value is tampered. It builds a
full VM trace, so it is a box test (lib suite), not run on the laptop.
The ZF FORMAT banner's fri field (fri=pair|dp) already exists (C2).
LAMBDA_VM_ZF_FRI=dp is now selectable: ZfFormat no longer aborts on it. Implemented: the CPU prover (group-leaf layer commits, scheduled folds, group openings) and the host verifier, owned and archived views. On a cuda build every device FRI arm runs only for fri = pair; a dp table takes the CPU FRI loop (DEEP may still run on the device). Not implemented: device group-leaf FRI (I-FRI-D); the in-guest LFM verifier of a dp proof (I-FRI-G: lfm::fri::FriShape still derives the legacy layout, so emitting a wrap or node over a dp proof fails its committed-layer assert); the RV64 recursion guest (default-only by RULINGS 11, it refuses a non-default format). So a block run at LAMBDA_VM_ZF_FRI=dp proves and host-verifies its STARK proofs but cannot recurse over them yet. The zf_format lever test now pins that fri=dp is not reported as unimplemented.
production_sites_prove_at_the_process_format proves and host-verifies a small ext3 STARK under RPX with block_base_options() and aggregation_wrap_options(), the two univariate production format sites, and checks the encoding the process format implies. Without a knob it pins today's legacy encoding; under LAMBDA_VM_ZF_FRI=dp (the box's knob-on line) it asserts both sites stamp FriMode::Dp and the proofs carry group layers. Checked on the laptop both ways (the dp run prints "ZF FORMAT: ... fri=dp ...").
…path lengths in the STARK verifier, and the ZfFormat skeleton C1 ab7208f adds the cap primitive and the auto cap-height policy (height at most 3, chosen by the recursion cost law). C1b f82e42b makes the host STARK verifier require exact authentication-path lengths. C2 77ea1ab adds ZfFormat, the one proof-format config, parsed once from LAMBDA_VM_ZF_*; every lever is unimplemented at this commit, so any knob aborts and the default is byte-identical. Gates on FAST at 77ea1ab (default format): prover lib 1466 passed / 0 failed / 82 ignored (base 1456 + 10), stark 325 / 0, crypto 158 / 0, multilinear 310 / 0, rpx device parity 11 / 11, math-cuda 207 / 0, whir_transcript_configuration (hash-metrics) 3 / 0, byte and identity gates green.
Merges d281c3b (lane I-CAP-W, zf/cap-whir): Merkle caps on WHIR chains, host (C6), device parity tests (C7) and in-guest (C8), and WHIR_CAP_IMPLEMENTED = true. Conflicts resolved: - prover/src/zf_format.rs (tests): I-CAP-S added the_merkle_cap_knob_is_selectable and I-CAP-W added the_whir_cap_is_implemented_and_selectable at the same spot. Both tests are kept verbatim; no other hunk conflicted.
Merges ac73346 (lane I-WHIR-F, zf/whir-folds): WhirFolds::First, with_security_folds, the statement fold word, committed_under in agrees_with, the production config under the format, GPU k = 6 parity tests, in-guest k = 5/6 gates, and WHIR_FOLDS_IMPLEMENTED = true. Auto-merged without conflict: crypto/multilinear/src/whir_chain.rs (with_security delegates to with_security_folds; tree_caps derives from config.schedule(), so W1 caps follow the W2 schedule), math-cuda whir_commit.rs / whir_fold.rs tests. Conflicts resolved (tests only, no behaviour change): - prover/src/zf_format.rs: the_whir_fold_lever_is_selectable added at the same spot as the two cap-selectable tests; all three kept verbatim. - prover/src/lfm/whir_chain_tests.rs: - imports: the union (CapPolicy from I-CAP-W; ChainFormat, FirstFold, WhirFolds from I-WHIR-F). - both lanes introduced a helper named fixture_with with different signatures. I-WHIR-F's general fixture_with(&ChainConfig, num_vars) keeps the name; I-CAP-W's (num_vars, Q, grind, cap) helper is renamed fixture_capped and now builds config_with(Q, grind, cap) and calls the general one (the same config it built before). Its three call sites in the W1 section are renamed; nothing else changed. - the two appended sections (W1 cap tests, W2 first-fold tests) are both kept verbatim, W1 first.
Merges 6092c77 (lane I-FRI-H, zf/fri-host rebased on 77ea1ab): the cost-law FRI schedule DP, the fri_schedule_override test hook, S3 group FRI on the CPU prover and host verifier, goldens and vectors, and FRI_MODE_IMPLEMENTED = true. Auto-merged without conflict: crypto/stark/src/proof/options.rs (ProofFormat now carries merkle_cap, fri_mode, one_row and fri_schedule_override; MERKLE_CAP_IMPLEMENTED and FRI_MODE_IMPLEMENTED both true), prover/src/zf_format.rs (proof_format sets the override to None), crypto/stark/src/tests/mod.rs. Conflicts resolved: - crypto/stark/src/prover.rs, round 4: - the query phase: I-CAP-S made query_list mutable (the cap post-pass embeds caps into it); I-FRI-H switched it to query_phase_with_layout. Resolved as a mutable binding of query_phase_with_layout(&fri_layers, &iotas, &fri_layout). - I-CAP-S's embed_stark_caps / tree_cap helpers were one side of an add/nothing hunk; kept verbatim. - crypto/stark/src/verifier.rs (textually clean, semantically broken, fixed without changing either lane's behaviour): - table_tree_checks (I-CAP-S) read fri_termination_params(..).num_committed, which I-FRI-H changed to return Option. Now `?`: a format the verifier cannot lay out makes table_tree_checks None, which rejects the proof, the same verdict step 3 gives it. - I-CAP-S removed step 3's `lde_log` binding (its legacy path takes the per-tree checks instead); I-FRI-H's group path still passes lde_log to verify_query_groups. The binding is restored, with I-FRI-H's comment, before the terminal codeword. Not resolved here (reported to the lead, no code change): StarkCaps derives FRI layer depths from the legacy layout; the group (fri=dp) verifier path authenticates full paths and ignores FRI caps. So cap on together with fri=dp fails closed (prover depth Err or verifier rejection), a completeness gap, not a soundness one.
Under a fold schedule (fri=dp) a committed FRI layer is a group tree whose
depth is the fold layout's, not log2(lde) - j - 2. StarkCaps took the FRI
depths from the pair layout, and the group-path verifier authenticated every
layer with an uncapped CappedRoot, so LAMBDA_VM_ZF_CAP with
LAMBDA_VM_ZF_FRI=dp failed closed (M-MERGE-B note 2, REVIEW-FRI F9).
- StarkCaps::from_layout / for_options: FRI depths from FriFoldLayout;
the prover (round-4 cap post-pass) and the verifier (table_tree_checks)
both build from the layout they already hold. StarkCaps::new stays the
pair-layout form for existing callers.
- fri::group::verify_query_groups authenticates layer j with the tree's
TreeCheck (exact length D - c, query 0 the cap's owner, cap-to-root once
per tree) instead of an uncapped root check.
- Default format unchanged: at cap=off every height is 0 and TreeCheck is
the C1b exact-length check the group path already ran.
Tests (cap_fri_matrix_tests): {off, fixed(2), auto} x {pair, dp, dp [3,1,3]}
at Q=24 round-trips owned and archived with the layout-depth capped path
shape; every cap node of a capped group layer is bound; an unreached cap
node is rejected by the cap-to-root check alone; a proof made under one
(cap, fri) cell fails under the others.
The (d) proof vectors ran at Q = 3, where the auto cap policy caps nothing (RULINGS 1: height 0 below 4 openings), so no vector exercised S1 with or without S3. Two formats are added for Keccak, Blake3 and RPX at Q = 20: cap_pair (cap=auto, fri=pair) and cap_dp (cap=auto, fri=dp), every tree capped at height 3. Their JSON also records the verifier's StarkCaps (trace/FRI depths and heights). The existing pair/dp/dp_3_1_3 files are byte-identical (proof_options takes the query count; the new JSON lines are written for capped formats only). cap_dp's FRI roots and zetas equal dp's: the cap moves no transcript value.
verify_query_groups read the layer roots off the proof; it authenticates with the per-tree checks since the previous commit, so the parameter was unused (a -D warnings lint failure).
A committed table carries no name, so each ARGUE FUSED line gives its signature - roots, bus terms, walk slots - beside its factor count, and a declined table prints a line of its own under the cross-check or LAMBDA_VM_ARGUE_FUSED_LOG. LAMBDA_VM_ARGUE_INT_NODES=1 prints one banner when it is first read, so an arm's log shows it took effect.
The upload declines a table under 4096 cells (gpu::worth_the_device), and the prover then argues it on the host, so a run at 2^8 of EQ's 12 factors never reached the card: FAST job 271's one red. Each table now runs at 2^8 or the first height above it with 4096 cells.
A table without roots has a zero constraint part and d_C = 0, so its
grid {0,1}^2 is all corners; with the corners skipped - the production
setting, no cross-check - no grid point is left, and the launch sizing
divided by that empty row count. FAST job 273's B arm panicked there
("attempt to divide by zero", argue_fused.rs:101) at the first such
table; its X arm, whose cross-check computes the corners, proved and
verified with all 390 fused tables confirmed.
An empty point list now launches nothing (T is zero) and sizes no slot
file; U is still computed. A host test pins the sizing (it reproduced
the panic at the same line before this change). Two card tests close
the gap that let it through, both with the production switches: every
table without roots against today's host rounds, the corners skipped;
and test_keccak proved under the B arm's switches, with and without the
cross-check, and verified.
The FAST A/B at 9e27289 read EFFECTIVE twice (jobs 274 and 270, pooled over 4 A and 4 B arms): base -2.80 s, the argue -2.94 s, the whole run -2.75 s, every B arm's base below every A arm's, identities equal on all eight arms, no fallback; the cross-check arm confirmed every one of 390 fused tables' messages against today's rounds. LAMBDA_VM_ARGUE_FUSED and LAMBDA_VM_ARGUE_INT_NODES are now on unless set to 0, and 0 is today's rounds exactly. Each prints a banner when first read, and a unit test pins each default. A fused session counts as a device sumcheck (gpu::sumcheck_calls, sumcheck_rounds), and the split's ARGUE ZEROCHECK line ends with the fused sessions, the declined ones and their device time, so an arm's log shows which rounds it ran.
…is refused With the fused zerocheck on by default, the tall-table knob tests pin it off: every other argue knob acts on today's rounds. Two tests on top: the tall tables proved with the fused rounds (alone, and with the device columns, tables and gathered reads) give today's canonical bytes table by table and whole, the same transcript and next challenge, and verify - on a device the fused arm shows its sessions; and with the fused rounds' bus coefficient off by one the proof parts from today's at CPU and does not verify. The fused faults are per thread now: the fused rounds run by default, so a fault armed for one test must not reach a proof another test runs beside it, and a table's argument runs on the calling thread.
MauroToscano
added a commit
that referenced
this pull request
Sep 30, 2026
The process pool kept its two 3.22 GB slots for the life of the process. On #1010's production tree the host peak is in level 1 (16.2 GiB against the base's 9.6), where no epoch needs a slot, so kept slots would add all 6.4 GB of them to the whole run's peak. D-TRACE-1B §3.4 sized the base's peak only. SlotPool::release_free frees every block nobody holds; a later fill makes them again, and until then a lease misses as not ready. The WHIR base calls it on a helper as soon as the last epoch is proved, beside the cross-epoch proof, and joins the helper before it returns (PINNED SLOTS: released … line). Tests: releasing frees only unheld blocks, a held block survives and comes back, the next fill remakes them (heap blocks, laptop); the one-slot pipeline test now asserts the slot is back and released after the run.
MauroToscano
changed the title
…AMBDA_VM_ARGUE_GKR_GRUEN
D-ARGUE S1-3 (D-BATCH M1-1). A device GKR layer's round sends
s(t) = E·eq1(u_j, t)·H(t), with H(t) the layer's h summed under
eq(u_{>j}, ·). The card now sums H(1) and H(2) only - every node by
additions, no eq factor and no program walk - and folds the previous
challenge on the way in; the host puts E·eq1 back, takes H(0) from the
claim (the card sums it where 1 - u_j has no inverse) and extrapolates
H(3). The weight is two small tables a layer (the tail's variables and
one level per card round), not a layer-sized eq table folded each round.
The rounds stop at a cube of LAMBDA_VM_ARGUE_GKR_GRUEN_TAIL (default 64)
and hand the host today's five factors there.
Every message is today's field element, so the transcript and the
canonical bytes do not move. Off by default: off is today's rounds.
- math-cuda: kernels gkr_eq_levels_ext3, gkr_round_gruen,
gkr_gruen_finish; GruenLayer (tree layers and the rebuilt input
layer); SumcheckSession::fold_first for the cross-check's shadow.
- multilinear: gkr_gruen (knobs, the host's half of a round, counters,
a per-thread fault, a host reference of the device algorithm);
DeviceTree::prove_layer_gruen; LAMBDA_VM_ARGUE_GKR_GRUEN_XCHECK walks
today's program over the same folded halves each round and compares
rounds and factors; the ARGUE GKR line ends with the Gruen counts.
- tests: the host reference equals today's rounds, challenges and
factors at m 1..9 over every tail split, with H(0) direct or derived,
and with coordinates of one; a wrong claim changes it. Device tests
(tests/argue_gkr_gruen.rs) and stark's tall-table byte identity and
fault test run on a card.
…GRUEN=0 the opt-out FAST job 330 (4 + 4 arms on #1010 + Q1b): base -1.77 s, the argue -2.08 s, the whole run -1.57 s, the GKR 4.24 -> 2.13 s, the same program ids; its cross-check arm compared 3,381 real layers with the old rounds and found every one equal. A unit test pins the default.
MauroToscano
changed the title
…H S0) Under LAMBDA_VM_BASE_SPLIT only, and byte-identical: the argue's "rest" - what is neither a device GKR layer nor a zerocheck round, 3.19 s a block known only by subtraction - is timed per region of a table's prove: interactions, tree, output, gkr (its host prefix apart), setup, batch, factor values, claim reduce, column evaluation, release. One `ARGUE REST #k` line an epoch sums them against the argue's wall, and one `ARGUE AIR #k t NAME` line a table gives the shape D-BATCH's plan is sized from (n, columns, factors and how many read a shifted row, interactions, k, degree, roots, widest bus message) with its tree, gkr and core times.
Under LAMBDA_VM_BASE_SPLIT, an ARGUE TREE line an epoch splits the tree region S0 measured at 1.80 s a block: the factors lifted, the input layer's programs lowered and written, the levels folded, the output read. The card runs the first three asynchronously, so LAMBDA_VM_ARGUE_TREE_SYNC=1 (a diagnostic, never a wall measurement) makes each part wait for its own kernels and charges it its card time. Byte-identical.
…d LAMBDA_VM_ARGUE_GKR_INPUT D-BATCH M1-2, its first half. The tree region measured 1.80 s a block, and its card time is mostly the input layer's writes (1.42 s of 2.39 s under the sync split, FAST 332): two program launches an interaction, each walking ext3 lifted factors through a slot file of its own. Under the knob one launch writes every interaction's two sides straight from the table's resident base columns - `constant + sum coeff * column` as base x ext3 products, the same field values - from a plan built once a table (`logup::input_plan`) and kept for the layer's rewrite. The tree, its output and the GKR proof are the same; the factors are still lifted, for the zerocheck. Off by default; off is today's path. - math-cuda: kernel gkr_input_from_columns; gkr::InputPlan and gkr::input_from_columns. - multilinear: the tree builder takes a writer (the lifted one or the columns' one), input_layer_tree_from_columns, logup::input_plan and resident_tree_from_columns, TraceData::resident_shared, a counter, and a test hook that hands every input layer back so its rewrite is reachable. - tests: the plan's cells equal input_layer over the lifted factors (direct and shifted columns, padded or not; a mutated shift fails it); a public factor has no plan; on the card (tests/argue_gkr_input.rs) the columns' tree proves today's proof carried and handed back, and a wrong constant moves the output; stark's tall tables give today's canonical bytes with the knob alone and beside the production defaults.
…AMBDA_VM_ARGUE_NO_LIFT D-BATCH M1-2, its second half. With the input layer written from the columns (LAMBDA_VM_ARGUE_GKR_INPUT), the only reader of the lifted factors left is the zerocheck, and the fused rounds' first pass reads only their base limb. Under the knob a table's factors stay its resident base columns: the fused kernels take a row stride (3 for lifted factors, 1 for base columns), a public table is a base copy, and the W*rows*24 B lift is made only when today's rounds need it - the fused rounds declined, or the cross-check replays today's beside them. The same rounds and proof. A table the columns cannot stand in for (a shifted factor, a public table above the base field, no fused description) is lifted as before. Off by default; it needs LAMBDA_VM_ARGUE_GKR_INPUT. - math-cuda: zc_grid01, zc_bus_u, zc_fold2 take a stride; sumcheck::FactorView (the fused session's source) and ColumnFactors. - multilinear: gpu::ColumnFactors and column_factors, gpu_fused's FusedSource and FusedInput::columns, batch::prove_resident_lazy (the lift made late, counted), the knob and counters; the ARGUE TREE line ends with the trees from the columns and the tables with no lift. - stark: the tall tables' canonical bytes with no lift beside the production defaults.
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
…TER_LAST=0 the opt-out FAST job 255 (A B B A, 4 + 4 arms at #1010's head 7d82a32): level 1 -0.40 s, the whole run -0.43 s, the base -0.05 s, the same five program ids in all eight arms. Without the latch the global child took the card before the last wide node's artifacts in 3 of 4 arms; with it, in none. The knob's parse moves into global_after_last_from, so a unit test pins the default and the opt-out without touching the environment, and a second one pins the refusal of any other value. The banners now say the lever is on by default and name =0 as the way off; their leading text is unchanged, so the gate and readout scripts still match them.
…fault LAMBDA_VM_ARGUE_GKR_INPUT=0 writes the input layer from the lifted factors again; LAMBDA_VM_ARGUE_NO_LIFT=0 lifts every table's factors as before (no lift needs the input from the columns, and its banner says so when that is off). FAST job 333 (input from the columns, 4 + 4 arms on #1010's head): base -0.75 s, the argue -0.97 s, the whole run -0.73 s, the tree region 1.98 -> 1.11 s. FAST job 335 (+ no lift, 4 + 4 arms): base -0.90 s, the whole run -1.55 s, the argue's reserved peak -1.5 GiB, kept WHIR trees evicted 13 -> 2 a run and the openings' tree rebuilds 0.74 -> 0.04 s. Every arm of both on the record's program ids. Unit tests pin both defaults.
…'s artifacts (LFM_TREE_GLOBAL_AFTER_LAST, default off) Level 1 ends when its last wide node proves, and that node's chain is its prologue, its artifacts, its host prep and its prove. The global child's prove fits inside that prep at no cost. But the global's card request and the last node's artifact request arrive within a few hundred milliseconds of each other, near 5 s into level 1. In 34 arms (jobs 246-292) the global asked first 11 times, and all 11 read level 1 at 8.0-8.7 s. Each time the last node's artifacts waited out the global's whole prove, and its prep then ran with the card idle. No arm under 8.0 s had the global first. Under LFM_TREE_GLOBAL_AFTER_LAST=1 the global's multi_prove waits behind a latch that the last wide node opens once its artifacts are built. The global's host prep keeps its place; only its card request moves. device_permit gains CardLatch, OpenOnDrop and a thread-local deferral that applies only to multi_prove holds on an armed permit. The deferral waits before the queue, never in it, and at most 30 s, after which it queues anyway and says so. Each deferral prints a CARD DEFER line. The driver applies the lever only to a wide level 1 whose pool runs the global child with a worker for every task, so the global can never wait for a node no worker has taken; otherwise it prints why the lever is inactive. The last node's opener also opens the latch as its task unwinds. Only scheduling changes: no proof byte moves.
A level's tasks run one to a thread. The driver now names each task's proof (the global child, a wide node, a wrap) in a thread-local, and each CARD HOLD and CARD DEFER trace line ends with "· who=<name>". The suffix comes after the closing bracket, so existing parsers of these lines are unaffected. This lets the global-after-last A/B read the card order directly (whose multi_prove came before the last node's artifacts) instead of inferring the holders from their timing. Trace-only: nothing is named when LFM_CARD_TRACE is off, and the untraced permit path allocates nothing.
…h no global in the pool The lever's activity is now an explicit mode (Off, Active, NoGlobalInThePool, TooFewWorkers), and every case prints what it does when the knob is set. No global child in the level's pool covers a level of wraps, LFM_TREE_TOP_OVERLAP=0 (the global runs as its own stage) and the fixture tree. In all of those no latch is made and nothing waits. Small blocks follow the worker count. Two to fan-in epochs are one wide node plus the global on at least two workers, so the global waits for that node's artifacts. A one-epoch block runs on one worker and does not take the lever. Unit tests cover these cases next to the deadlock guard's. A device_permit test covers a thread with no deferral and an opener nobody waits on.
…TER_LAST=0 the opt-out FAST job 255 (A B B A, 4 + 4 arms at #1010's head 7d82a32): level 1 -0.40 s, the whole run -0.43 s, the base -0.05 s, the same five program ids in all eight arms. Without the latch the global child took the card before the last wide node's artifacts in 3 of 4 arms; with it, in none. The knob's parse moves into global_after_last_from, so a unit test pins the default and the opt-out without touching the environment, and a second one pins the refusal of any other value. The banners now say the lever is on by default and name =0 as the way off; their leading text is unchanged, so the gate and readout scripts still match them.
MauroToscano
changed the title
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
… lift, latch) into argue/epoch-batch Conflicts resolved by keeping both sides: gpu.rs keeps #1010's prove_layer_gruen and the batched argue's LayerSession side by side; gpu_fused.rs keeps FusedStepper (prove_fused is a loop over it) and takes #1010's FusedSource, so a stepper reads the lifted factors or the base columns where they lie; lib.rs declares gkr_gruen and gkr_lockstep. The batched argue now runs where the per-table argue runs at that head. Its trees are written from the base columns with no lift, in the same order the per-table path falls back. Its fused rounds read the base columns (TableRounds takes the column factors), and a table they cannot read is lifted as the per-table path lifts it. It prints a phase split (trees, ladders, zc setup, zc rounds, reduce) under LAMBDA_VM_BASE_SPLIT=1. The measurement-only knob takes LAMBDA_VM_ARGUE_BATCHED_MEASURE_CAP to read a bin's peak at another cap.
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
WhirBlockPlan::derive takes the statement through the host verifier's own checks (block_frame), derives the prepared roots from the program, prices each group in permutations from the closed forms, and partitions the groups over the leaves (heaviest first onto the least-loaded leaf; leaf 0 carries the COMMIT-bus target). It never reads a proof. A leaf replays the statement as constants and the roots block over every root of the block (the groups' hinted, the prepared ones derived), then for each of its groups, on the fork S_post || g: the tables' arguments with their preprocessed legs, the group's opening, the prepared openings. These are #1010's epoch legs, unchanged. It publishes the block's id, the state, the output halves and its sum of p/q (minus the target on the carrier). Every count it hints comes from the shape (hint_table_wires_shaped, hint_group_chains_shaped); the arena builder refuses a proof whose argument has other shapes. The plan derives the top program with no proof, and verify_block_tree checks a top proof against it. Tests: - laptop: the group partition, by rule and by refusal; - run on the laptop with LAMBDA_VM_WHIR_HASH=rpx: the front draws the host's z, alpha, beta and a fork's first draw; a leaf refuses a tampered root, table argument and prepared opening, and without the prepared openings the last tamper executes; - box: the leaves close the bus; each node binding refuses its tamper over real leaves and is load-bearing, including a foreign leaf (state) and a carrier that subtracts nothing (bus); the tree proves to the derived top, and a tree over another partition is refused there; the real block's readout.
MauroToscano
added a commit
that referenced
this pull request
Oct 1, 2026
…as a knob The WHIR chains (base and W-LFM) ground 20 bits, a constant. The knob makes the bits a format parameter read at the one production config site (chain_config_under), so the prover, the host verifier and the in-guest emitters all take them from the process format, never from a proof. The query count already subtracts the query grind, so 18 bits raises Q from 112 to 114 at every production height (15..=27 variables); every proven phase keeps its minimum (binding phase: the unground fold at 27 variables, 130.393; query phases 130.926 -> 130.907). Unset is 20: today's configs and proofs, byte for byte. The banner gains whir_grind_bits=. A chain ground at fewer bits is refused by a stricter verifier on both the host and the machine, and a proof opened at a Q the verifier does not expect is refused. (cherry picked from commit 8c39b95)
…nd 18 grind bits Prints the emitted chain verifier's real rows per chip, production format, n 21..=27, under LAMBDA_VM_ZF_WHIR_GRIND_BITS 20 (Q 112) and 18 (Q 114): the per-chain deltas that size the recursion's table heights under the 18-bit arm. Asserts nothing; ignored. (cherry picked from commit 9d51421)
… bits unchanged at 130.393)
the_w_leg_costs_at_the_sizing_shapes pins the W-leg verifier's closed-form cost at the process format, and the 18-bit default opens two more queries a chain (wrap 0: +619 permutations under policy A, +596 under B), so the pins moved (FAST 665, the one lib-suite failure). A W-LFM plan refuses artifacts built under another config, so one process costs one setting: at 18 bits the test checks pins read from the 18-bit form; under LAMBDA_VM_ZF_WHIR_GRIND_BITS=20 it keeps the 20-bit pins and the design's 0.5 % instrument checks, which were taken at Q 112.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What made it fast, ranked
These are the optimizations that took block 25368371 from 104.2 minutes to 32.62 s, ranked by the speedup each
measured when it landed. Each row is its own before/after at that time, so the rows do not add up.
9e2728955) · 37.80 → 35.95 s atf3d359998eqtable, the host tail from a cube of 64 — the same messages¹ The move also changed the hardware, from a CPU box to one RTX 5090 on a Ryzen 9950X host.
² On a Ryzen 9950X + RTX 5090 box. The base alone fell from 156.3 to 67.9 s.
107.45 s, STARK 157.45 → 121.65 s. On STARK the caps add no wall on top of the 2^d folds, though they remove
another 1.4 M permutations.
161.4 s, 18 Sep), and is 1.84× faster today (32.62 against 60.18 s). Rows 6, 9, 10, 12, 13, 14 and 15, and most
of 17, are WHIR-only; row 7 and the one-row openings are STARK-only.
11.2× and 6.7× on 28 Sep.
The number
Block 25368371 on the FAST box (Ryzen 9 9950X, RTX 5090 32 GB), RPX commitments, 15 epochs at 2^21. The four
no-lift arms of the last A/B (FAST job 335, eight arms, A B B A A B B A) read 32.3, 32.7, 32.6 and 32.9 s (mean
32.62 s). They were measured at
ba784bd0bwithLAMBDA_VM_ARGUE_GKR_INPUT=1 LAMBDA_VM_ARGUE_NO_LIFT=1;d108cabb5is that commit plus the flip that makes both the defaults, so it runs the same code by default, and was gated, not
re-timed. The landing head
88b0d3196isd108cabb5plus the level-1 latch, on by default. The latch was timed in itsown A/B on
7d82a320f(job 255, −0.43 s), not on top of M1-2, so 32.62 s is quoted without it and the two gains are notadded. Host peak 16.3–19.9 GiB (the level-1 permit race of the M1-1 section, in both settings), device peak
26.4–27.1 GiB (27,122 MiB at most; the arms without no lift 28.9–29.2 GiB).
Each step below is its own ABBA on one binary: two arms per setting, alternated.
d1dc455145f15641b94ab853c6cb682091a333232d688bb7f5d8ee, its knob; default at73342bc66)22b81fc63, its knob; default at7c8272701)7c8272701d52f9dff6on9e2728955; two A B B A, pooled)f3d359998(eight arms)1946609c3+ the knob (eight arms)87ed8dbcd+ the knob (eight arms)ba784bd0b+ both knobs, over M1-2a (eight arms)208e2ff06+ the knob, on7d82a320f(eight arms)¹ Measured on its stage branch (
34c17603b), before P2-W and A1.² Two builds, alternated X XF X XF, at
6a6e26611: the MDS fix has no knob.The keep-futile and whole-trees rows are each the decision A/B on the head before it; the row after them is the pair's
at-head A/B (A =
LFM_WHIR_KEEP_FUTILE=0 LFM_WHIR_WHOLE_TREES=0). The stage-1 rows are its decision A/B (job 274 andits replication, job 270) and its at-head A/B (A =
LAMBDA_VM_ARGUE_FUSED=0 LAMBDA_VM_ARGUE_INT_NODES=0); at that headthe whole-tree retention takes back 0.52 s of the stage's base gain (see its section). The M1-1 row is its decision
A/B (job 330) on
f3d359998, the stage-1 head;7d82a320fis that A/B's B setting as the default. The M1-2 rowsare its two decision A/Bs (jobs 333 and 335) on
7d82a320f;d108cabb5is the second A/B's B setting as thedefault. The latch row is its A/B (job 255) on
7d82a320f, beside the M1-2 A/Bs rather than on top of them, with fourarms a setting (t ≈ −1.3; see its section);
88b0d3196isd108cabb5plus the latch with that A/B's B setting as thedefault.
In the third row's A arms, every fix in the next table is switched off by its opt-out. Their program ids and census equal
those before the batch (
668a89a4c). The one change with no opt-out of its own, the WHIR encoding through the engine,is in both arms. A fifth arm, the defaults with only the level-0 lead-in off, read 61.4 s, so the lead-in is worth
−1.20 s here. The STARK PR (#1009) measured the same batch at −28.75 s (107.55 → 78.80 s).
The gap fixes
Each fix was measured first in its own ABBA, mostly on the base before the engine. Those rows do not add up to the
cumulative −39.65 s; the last row above is the measurement.
LAMBDA_VM_ZF_WHIR_STACK=25LAMBDA_VM_RPX_LIMB_PERMUTE=0LAMBDA_VM_RPX_GRIND_QUEUE=0LAMBDA_VM_BASE_PREP_ON_PROVER=1LAMBDA_VM_LFM_KEEP_BITWISE=1LAMBDA_VM_RPX_WARP_MERKLE=0LFM_TREE_PROLOGUES_AT_LEVEL0=1d1dc45514LAMBDA_VM_WHIR_FOLD_CLASSIC=1LAMBDA_VM_STAGING_SHARED_SLAB=1LAMBDA_VM_NO_WHIR_FUSED_FOLD=1,LAMBDA_VM_WHIR_LEAN_ROUNDS=0LFM_TREE_REDERIVE_DECODE=1LAMBDA_VM_LDE_LEGACY=1, which also reverts every other LDELAMBDA_VM_DEEP_INV_LEGACY=1LAMBDA_VM_NO_WHIR_ROOM_PARK=1,LAMBDA_VM_NO_WHIR_ROOM_RESIZE=1LAMBDA_VM_LFM_HASH_SPLIT=1turns it onAlso in the batch, with no knob:
Grinding only before the queries (P2-W)
What changed. Each round of a WHIR base chain used to grind 20 bits before three challenges: the first folding
challenge, the out-of-domain batching challenge γ and the query positions. It now grinds before the query positions
only.
1,472.
whir_grind, defaultquery; the banner reads… whir_stack=27 whir_grind=query.The proof carries only the nonces it spends (
NonceLayout::Spent).1,036 fewer a block.
nonzero value in a field the format does not carry.
Measured on block 25368371 (FAST, one binary, arms A B B A, wt820–823):
LAMBDA_VM_ZF_WHIR_GRIND=allpredicted from the grind count.
Soundness: no proven bits are lost. Of a round's three grinds, only the query grind raises the proven minimum as
placed:
challenge by varying that message, without grinding again, so this grind earned no credit.
with no grind at all.
Every phase keeps its bits:
security/zisk_calc.py).[0,0,20]against[20,20,20]), so a proofground one way does not verify the other.
red.
Opt-out.
LAMBDA_VM_ZF_WHIR_GRIND=allrestores the grinds before all three challenges and the three-nonce format:the previous proofs, program ids and census, byte for byte. Golden tests on the chain programs, arenas and host proof
bytes pin it, and so does the A arms' match above.
The argue's short, wide tables on the GPU (A1)
What changed. In the WHIR base's argue, a table whose columns are already resident on the card is now valued there
once it holds 2^16 cells (width × rows). Before, each column needed 2^16 rows. The few columns left on the host are
walked across the thread pool.
fall from 24,195 to 3,478 a block.
Measured on block 25368371 (FAST, one binary, arms A B B A):
LAMBDA_VM_ARGUE_DEVICE_COLUMNS=093a2b5643, wt831–834)8930490e5, wt850–853)The whole saving is in the base (41.90 → 40.95 s in the stage's ABBA); level 0 and the interior stay within noise.
Soundness: the proof does not change. The card computes each column's multilinear value exactly, the same field
element the host computes, so the transcript, every challenge and the serialized proof are identical, and so are the
program ids and census.
LAMBDA_VM_ARGUE_XCHECK=1) re-evaluated every card value on the host: 30,086 of 30,086 matched.on the card; a wrong card value is refused.
Opt-out.
LAMBDA_VM_ARGUE_DEVICE_COLUMNS=0restores the height rule and the one-at-a-time host walk, line for line.The argue's challenge tables on the GPU (A2+A3)
What changed. The WHIR base's argue built its challenge-dependent tables on the host and uploaded them: the
zerocheck's
eq(r)andeq(row)weights, and the claim reduce's shift tables and batched columns. It now builds themon the card from the columns already resident there.
eq(α)table; each batched column is one kernel over theresident columns.
pageable uploads a block (1.16 s of copies).
Measured on its stage branch (
34c17603b, before P2-W and A1; wt836–839): A 59.65 s (59.5, 59.8) → B 54.45 s(54.4, 54.5), −5.20 s. The base fell 41.65 → 36.65 s and the argue 19.7 → 14.7 s; the card built 1,364 tables an
arm.
Soundness: the proof does not change. The card builds the same field elements the host built, so the transcript,
every challenge and the serialized proof are identical.
LAMBDA_VM_ARGUE_XCHECK=1) compared every card table with the host's before its first round.the fault inert fails that test.
Opt-out.
LAMBDA_VM_ARGUE_DEVICE_TABLES=0builds the tables on the host and uploads them, as before.Pure WHIR recursion
What changed. The recursion's LFM proofs (the global wrap, the nodes and the block-artifact root) are proved by the
base's own stacked-WHIR prover instead of one STARK per table. Each parent verifies a child with the WHIR verifier the
wraps already run, over the child's LFM statement.
three times, then the node's own bindings and publishes. The 15 wraps and their proofs are gone. With three epochs a
node, the tree's fan-in, the node schema, the root's L2G fold and every level above are unchanged.
own point. The main stack holds the value columns only.
harvests and the emission.
global wrap's program is the same one.
Measured on block 25368371 (FAST, one binary per row, arms A B B A):
4150afab6, wt860–863)6a6e26611, wt880–883; A =LAMBDA_VM_LFM_PROVER=stark)against the wraps' 7.4 s, the interior 1.8 s against 9.0 s, the root 1.0 s against 1.4 s.
≥ 4. The base is 9 s faster than when that row was set, which leaves the two helpers a 4.7 s tail. The property the
count stood for held: the GPU's first hold came 0.17 s after level 1 started.
Soundness: every phase keeps ≥ 128 proven bits, and the recursion's minimum rises.
(114 queries and an 18-bit grind since the grind-18 change below), stacks of 2^24–2^27. Their minimum is 130.393 bits, the n = 27 first fold, unground, the same as the base's. It
replaces the STARK recursion's 128.946 bits, which came from its LFM query phase. Measured by the calculator on each
run's own chain lines.
statement built from the AIR's column list would count zero and bind nothing: a forged program would verify.
statement. The sponge receives each as a base token, so a non-canonical upper lane is unprovable.
next one's INIT, each epoch at its tree position. It reads these from what the wraps would have published. Its L2G
item is the fold of the epochs' bookend roots, the fold a node over those wraps takes.
AIR's count. A forged instruction column is refused by the prepared opening. A deleted opening, a restated table
height, a tampered or reordered public word and a prepared root absorbed after
zare each refused.that nothing settles are each refused.
disagreeing attestation id are each refused, each beside a control without the bindings that executes.
verifies with the count at zero and is refused with the AIR's count.
Opt-outs.
LAMBDA_VM_LFM_PROVER=starkrestores the per-table STARK recursion. The A arms above print8930490e5's 24 programids byte for byte.
LAMBDA_VM_LFM_WHIR_PREP=bothalso keeps each table's instruction columns in the main stack.LAMBDA_VM_LFM_WIDE=offkeeps the wraps under the WHIR recursion.Narrow sumcheck rounds on demand (N1′)
What changed. In the WHIR argue's zerocheck, a big batch's device rounds now walk its program on demand.
Each step is emitted where the step that uses it first needs it, in Sethi–Ullman order: of two operands, the one
needing more values goes first.
Every read, a column's value or a constant, is emitted again at each use instead of once and held.
The steps are the same operations on the same operands. What changes is how many values a thread holds at once,
which sizes the round kernel's per-thread slot file and so how many threads a round can run.
The slot file is also sized for every interpolation node from the first round.
A batch is big when its program holds more than 341 values a thread, which leaves a round under 64 k threads at the
512 MiB slot budget. Five batches are big:
Every other batch keeps its program as it was, the byte gate's EQ fixture (26 values) included.
Measured on block 25368371 (FAST, one binary):
LAMBDA_VM_ARGUE_LEAN_PROGRAM=0965e13de2, wt890–894)a28ad36af, wt910–914)Where the gain lands: the base.
fell 1.28 s.
2 of 5 programs are ready, and the card waits in the gaps between them, so the saving does not reach the wall.
column values instead of 331, over up to ≈ 4 GB of columns.
Soundness: the proof does not change. The program on demand is the same steps on the same operands in another
order, so every round's values are the same field elements.
and the census: equal in every arm of both runs.
LAMBDA_VM_ARGUE_XCHECK=1) walked the old program in a shadow session over the same card-residentvalues. It compared every big session's rounds, round by round, in the base and in every W-LFM proof, and every one
matched.
BatchMismatch), and by the cross-checkbefore a proof exists (
DeviceFailed);Opt-out.
LAMBDA_VM_ARGUE_LEAN_PROGRAM=0keeps every batch's program as before and sizes the slot file for onethread an index, line for line.
The RPX MDS compiled the same way in every build
What changed. Both RPX implementations compute the MDS over a compile-time circulant with plain loops, instead of a
core::array::from_fnclosure. The closure's wrapper was inlined only when rustc's codegen-unit partitioning placed itin
mds's own unit; otherwise each output lane was an out-of-line call. That made the host's hashing about 20 % slowerin some builds than in others, decided by unrelated edits.
Measured at
6a6e26611(two builds, X XF X XF): −0.50 s (45.65 → 45.15 s). The executor's hashing runs at0.81 of its old time per permutation; most of the gain is in the base (−0.30 s). The STARK PR (#1009), where host
hashing sits on more of the critical path, measured −5.95 s.
Soundness. The same values: the RPO and RPX known-answer vectors, the two implementations' agreement test and a new
test against the circulant's definition pin it, and transposing the matrix fails six of them. No knob.
The card permit after the host prep, and fan-in 4
What changed.
them, the prefix check) is host-only work. It used to run inside the exclusive permit, with the card idle and locked:
1.68 s of level 1's card holds at job 222. It now runs while another proof holds the card.
the block-artifact root takes them directly beside the global wrap.
prove and +0.3 s in its emission, census and build.
LAMBDA_VM_LFM_PROVER=stark,LAMBDA_VM_LFM_WIDE=off) keep fan-in 3, and the STARK tree keeps 2.Measured on block 25368371 (FAST, one binary per row, arms A B B A):
533a22926, wt960–963)5f15641b9, wt970–973)533a22926, wt980–983)because the wall replicated: the whole-run row hit its pre-registered band in all three, each beyond its A arms'
spread (0.20 s).
and the tree takes the fan-in-4 shape.
Soundness: nothing a proof commits to changes. The tree's shape does change, and the verifier already takes any
arity.
three at a time, give the same proofs (
card_after_prep_tests). The prep never enters the device layer: every entryinto it is counted. The first A/B's program ids are equal across A and B.
root's L2G fold regroups the global wrap's roots exactly as the interior did. The root gates now include pure WHIR's
root (15 epochs at fan-in 4) in:
fallbacks. The root still publishes 180 words.
Opt-outs.
LFM_CARD_AFTER_PREP=0takes the permit before the prep. The proofs are the same.LFM_CENSUS_FAN_IN=3restores the previous pure-WHIR tree and its nine program ids.Fan-in 5
What changed. The wide pure-WHIR tree defaults to fan-in 5.
beside the global wrap.
LFM_CENSUS_FAN_INbound widens, to 2..=5. The STARK drivers keep 2..=4: nothing above fourhas been costed on them.
starkopt-out andLAMBDA_VM_LFM_WIDE=offkeep fan-in 3, and the STARK tree keeps 2.Measured on block 25368371 (FAST, one binary per row, arms A B B A):
8b2896c59, wt1000–1003)b682091a3, wt1010–1013)falls from 1.9 to 1.2 s.
270.9 M to 149.6 M cells.
The device peak after the base was 25,586 MiB.
slower, never wrong.
counted since
7650b53c7(a declined prefetch is not a fallback). The production tree at fan-in 5 reads 0refusals and 0 fallbacks.
LFM_CENSUS_FAN_IN=4is the opt-out.Soundness: nothing a proof commits to changes except the tree's shape, which the verifier takes at any arity.
node at two to five, two nodes at six.
Opt-outs.
LFM_CENSUS_FAN_IN=4restores the fan-in-4 tree and its six program ids.LFM_CENSUS_FAN_IN=3restores the fan-in-3 tree and its nine program ids.The WHIR base's head ahead
What changed. The WHIR base computes DECODE's univariate root on a helper thread, beside epoch 0, instead of
before the pipeline starts.
leaves over DECODE's columns), then the prepared DECODE commitment on the device. Only then did epoch 0 execute.
the thread that proves, and the DECODE derivation count stays on that thread.
it heard it before the pipeline. The level-1 lead-in reads it at its first claim, in the base's tail.
LAMBDA_VM_BASE_SPLIT=1: its start, the root, the prepared commitment and epoch 0'swait for the root.
Measured on block 25368371 (FAST, arms A B B A; all rows but the last are the decision A/B at
d117ffedd,wt1030–1033):
33232d688, wt1060–1063; A =LAMBDA_VM_WHIR_HEAD_AHEAD=0)executed.
waited 0.00 s.
1.10–1.11 s. Its collect, sharing the CPU with the root, grew from 0.32 to 0.52–0.54 s.
chain starts earlier.
Soundness: the proofs are byte-identical by construction.
The same values, only earlier. The root is the same pure host function of the ELF and the options
(
commitment_from_elf), computed on another thread. The prepared commitment is unchanged and committed in the sameplace. Epoch 0's preparation receives the same root. Only where and when the root is computed changes, never what
any proof commits to.
The test.
the_head_ahead_proves_what_the_serial_head_provesproves a run serial and ahead, under bothpreparation schedules. It compares:
It checks that the ahead bundle verifies, and that the observer hears the shared DECODE work once, with the serial
head's values, before any epoch is proved. It passed on the CPU build and on FAST's device build.
What the test does not compare: an epoch's first group root. Its rows follow
HashMaporder, so it differsbetween any two proves. The existing preparation-schedule test skips it for the same reason.
The tree: the 5 program ids are equal in all four arms and equal to the fan-in-5 landing's.
Opt-out.
LAMBDA_VM_WHIR_HEAD_AHEAD=0restores the serial head, with the same program ids. Any other value stopsthe run.
Keep the leaf layers through a futile budget miss
What changed. The WHIR retention no longer evicts its leaf layers for a device reservation they cannot rescue.
reservation misses the budget, the ledger asks the retention to drop layers until the deficit is covered.
through: it fails anyway, and each opening that needed a dropped layer hashes its leaves again.
gets the answer it got without this change.
futile misses N (M MiB kept).[gpu] WHIR retention: … (the pipeline default)or(LFM_WHIR_KEEP_FUTILE=0).Measured on block 25368371 (FAST, one binary, arms A B B A,
bb7f5d8ee, wt1080–1083; B =LFM_WHIR_KEEP_FUTILE=1,now the default):
budget, 1,346 MiB of room. It is now the base's epoch 4 argue: 25,034 MiB, 654 MiB of room. Epochs 3 and 5 peak
at 24,833 and 24,865. Each rose by exactly the layers it kept.
so a request there fails only when it is more than 1,470 MiB short. That was the threshold before too.
Level 1's argue still peaks at 24,342 MiB, unchanged in every arm.
time: a request the layers can cover evicts them and succeeds, as before this change. That epoch pays the old
re-hash and nothing more, so this change never refuses what the old code granted.
host, counted: device fallbacks and GKR tree refusals on the argue, commit fallbacks on the commit path. Slower,
never wrong.
The trigger, likely but not confirmed.
5.2–5.4 GiB.
multilinear::gpu::input_layer_tree_impl,reserve(eager)):Soundness: nothing a proof commits to changes.
tree, its root and its paths are the same either way.
a_miss_the_layers_cannot_cover_keeps_them_and_moves_no_pathtakes a futile miss both ways on thecard. It compares the root and the paths with a fresh codeword's.
=0, and diff each tree's five program idsagainst WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010's.
Opt-out.
LFM_WHIR_KEEP_FUTILE=0evicts as before. Any value other than unset,0or1stops the run.Keep whole WHIR trees on the card, evictable
What changed. A commitment now keeps its whole Merkle tree on the card, from its commit to its opening. Before, it
kept only the leaf layer.
the inner levels from it: one permutation a node, level by level. On the block that cost the openings 1.02 s of tree
rebuilds over 612 opens.
it, builds nothing and hashes nothing.
handed to the same evictor. A whole tree costs one more layer's bytes,
num_leaves − 1nodes.[gpu] WHIR retention: whole trees, the inner levels kept with the leaves (the pipeline default), orleaf layers, … (LFM_WHIR_WHOLE_TREES=0).whole trees on (N openings served).Measured on block 25368371 (FAST, one binary, arms A B B A,
22b81fc63, wt1084–1087). A = the keep-futilelanding's default (leaf layers). B =
LFM_WHIR_WHOLE_TREES=1, now the default.per commit, plus the two evicted trees.
(544 MiB), and their openings built them again.
bands.
VRAM: the reserved margin is gone in the heavy epochs. The margin before a fallback does not move.
of the 25,688 MiB budget. Epoch 5 comes within 7 MiB of the budget. Epoch 4 would reach 25,850 MiB: it evicts two
kept trees and peaks at 25,306.
for the trees it took.
GKR tree refusals on the argue, commit fallbacks on the commit path.
falls back is where it was before the change.
paths. An eviction in that window gives the tree's bytes back to the ledger while the buffer lives on until the path
gather ends. That is about 0.1 ms and at most one tree (≤ 512 MiB), and it falls inside the ≈ 3.4 GiB of card left
above the device peak.
H4, and why this is not it. H4 kept whole trees and lost about 15 s. Its trees sat outside any reservation, so a
full card made device allocations fail, and commits fell back to the host at about 1.5 GiB a chain. These trees are
reserved and evictable, and the tests now pin that invariant rather than "no tree is ever kept":
a_group_holds_only_its_codewords_before_any_open) runs in both modes. It checks three things:promise would read four trees there.
Soundness: nothing a proof commits to changes.
root and the paths are the same either way.
a_kept_whole_tree_serves_its_openings_and_moves_no_byte:the reservation, the blocking key, the process-wide identities, and the served / rehashed / evicted cap regimes.
=0, and diff each tree's five program idsagainst WHIR recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 32.62 s #1010's.
Opt-out.
LFM_WHIR_WHOLE_TREES=0keeps leaf layers as before. Any value other than unset,0or1stops the run.A kept tree's promise given back by its last handle
What changed. A kept whole tree now owns its ledger promise: the bytes go back to the device ledger when the
tree's last handle drops, not when its slot is emptied. An eviction or a codeword's drop while an opening still reads
the tree gives nothing back until that opening lets go, and the evictor passes over a tree an opening is reading
instead of counting it as reclaimable. This makes the transient under-count disclosed in the whole-trees section
unreachable. A request only a tree being read could cover now fails, counted, instead of being granted bytes the card
still holds; the window is one served opening's read.
· N kept tree(s) passed over: an opening was reading themwhen it happens.count read per entry. No timing A/B; the gates' production tree read as whole trees' (952 openings served, 2 trees
evicted, 3 futile misses kept, 0 passed over, the same five program ids).
a_kept_tree_an_opening_reads_stays_promised_until_the_opening_lets_goholds a readeracross a miss only its tree could cover, then across its codeword's drop, and checks the ledger at each step; two
mutations (the walk ignoring readers, the promise back with the slot) each fail it.
The argue's zerocheck computed the stage-1 way: same messages, a quarter of the device time
What changed. Each table's zerocheck batch —
eq(r,x)·C(x) + eq(ρ,x)·(γ·N(x) + γ²·D(x)), the constraint rulebeside the bus's two — is summed a different way on the card. Every round sends the message it sent before
(D-ARGUE §2.7: a round polynomial is a function of the batch, the challenges drawn before it and the round, so any
exact algorithm for it sends the same message).
γ·N + γ²·Dis one columnL = a₀ + Σ a_k·f_k, built once per table after the batching challenge. KECCAK_RND's2,062 interaction sides leave the per-row walk.
jisE^r·eq₁(r_j,X)·A_j(X) + E^ρ·eq₁(ρ_j,X)·B_j(X): the cardwalks the constraint part alone, at
X ∈ {0, 2..d}undereq(r_{>j}), and sumsL's two halves undereq(ρ_{>j});A_j(1)comes from the claim the round carries in.grid
{0..d}²in Goldilocks — each factor's grid by additions from its group's four rows — and both messages comeout of it; the grid's four boolean corners are zero on a trace that satisfies its AIR and are not computed. Both
folds then run at once, base to extension, into a quarter-size copy.
(k, 0, 0), sot·(hi − lo)is the componentwisek·(hi − lo):three products where the full multiply spends nine — in every device round, GKR and reduce included.
zc_grid01,zc_bus_u,zc_fold2,zc_bus_column,zc_halve,zc_round_gruen,sumcheck_round_ext3_int(math-cuda/kernels/sumcheck.cu); hostmath_cuda::argue_fused,multilinear::gpu_fused(the constraint program with an
ACCstep after each root),batch::prove_resident_with. The host reference ismultilinear::fused, which the card is checked against. The rounds stop at today's host crossover (cube 32) andhand today's host tail the same factors.
★ ARGUE FUSED: on (the default; LAMBDA_VM_ARGUE_FUSED=0 is today's rounds)and[gpu] sumcheck rounds: integer nodes (the default; …)once a run; each epoch'sARGUE ZEROCHECK #kline ends|| fused F (declined D) · M ms.Measured on block 25368371 (FAST, one binary, at 9e27289 + the change,
d52f9dff6; A = today's rounds, B =fused + integer nodes, now the default). Two A B B A jobs, the second a replication decided pooled with the first:
replication −2.70 / −2.85 / −2.94. wt1102's level 1 (8.6 s) is a single-arm outlier of the kind G6-LEDGER §9
documents; its whole run minus level 1 equals its twin's (29.4 s).
−0.06 s (integer nodes only; the GKR keeps today's round kernel — stage 1's S1-3 is not in this change).
factors in one process): KECCAK_RND 1,279 → 258 ms (R 0.20), CPU 1,094 → 288 ms (0.26), LFM_HASH 680 → 385 ms
(0.57); every fused table together 5,045 → 1,624 ms (0.32). Small and mid tables gained too: today's per-round cost
was mostly the walk of the whole batch, not launch latency.
At
f3d359998(FAST, eight arms A B B A A B B A, wt1105–1112; A =LAMBDA_VM_ARGUE_FUSED=0 LAMBDA_VM_ARGUE_INT_NODES=0, B = the defaults). The base and the argue decide; level 1 is reported:quarter-size folded copy,
L, two weights and its slot files). At that head the heavy epochs' argues already sit atthe budget with evictable kept trees, so the reservation takes them: each B arm evicted 10 kept trees instead of 2,
served 947 openings a kept tree instead of 952, and rebuilt 0.52 s more of trees. The argue's reserved peak read
25,660 MiB of 25,688 (A 25,681). Every fallback counter read 0 in all eight arms.
carry +0.8 s single-arm outliers of the kind G6-LEDGER §9 documents. Stage 1 acts on the base; the whole run minus
level 1 moved −2.32 s.
Soundness: nothing a proof commits to changes.
(D-ARGUE §2.7), and the only case where they would differ — a trace that breaks its AIR, under the corner skip —
gives a proof the verifier rejects either way.
LAMBDA_VM_ARGUE_FUSED_XCHECK=1, today's device rounds replay the fused challengesover the same factors and every message is compared, with the factors at the crossover, and the grid's corners are
checked per row: on the block, 390 of 390 fused tables confirmed, the root proved and verified (job 273, wt1092).
stark::multilinear_table::tests::the_argument_proves_the_same_bytes_with_the_fused_roundsproves the tall tables with the fused rounds, alone and with the other argue knobs, and compares the canonical proof
bytes table by table and whole, the transcript and the next challenge with today's; it runs on the card in the gates.
prover::tests::argue_stage1_tests, run alone): the fused rounds against today's host rounds onevery VM table and W-LFM chip, the three heaviest at 2^10 and 2^12 (42 runs, each confirmed by the replay); the
twelve tables without roots under the production switches;
test_keccakproved with the fused rounds and verified,with and without the cross-check; the integer-node rounds.
on the card is refused by the cross-check; a trace that breaks its AIR is refused by the corner check; a wrong bus
coefficient in a proof parts from today's at the first table and does not verify.
without constraints (its grid is all corners, so with the corners skipped no grid point was left, and the launch
sizing divided by zero). A prover panic, not a wrong proof; fixed before any number above was taken.
Gates. FAST2 job 177 at
land/1010-argue-q1b(f3d359998): 16 steps, all green — the lib suite 1,640 / 0 /100, math-cuda 279, stark 420. Besides the standard steps: the defaults pinned on the host; the card tests (42 fused
runs, the twelve rootless tables,
test_keccakproved and verified both ways, integer nodes) and both mutations red;real traces under the cross-check, none parted;
-p multilinear --features cuda --lib(368) and-p stark --features cuda,multilinear/cuda --lib multilinear_table(33, the canonical-bytes test on the card among them); the productiontree at the defaults (298 fused sessions over the base epochs, 947 openings served, #1010's five program ids) and under
both opt-outs (no fused session, the same ids).
Opt-outs.
LAMBDA_VM_ARGUE_FUSED=0runs today's zerocheck rounds exactly;LAMBDA_VM_ARGUE_INT_NODES=0today'sround kernel. Tables are also filtered by committed width with
LAMBDA_VM_ARGUE_FUSED_WIDTHS(unset: every table).The argue's GKR layers with Gruen's split (M1-1): same messages, half the GKR time
What changed. A device GKR layer's relation is
eq(u,x)·h(x),h = p_lo·q_hi + p_hi·q_lo + λ·q_lo·q_hi. Roundjsendss(t) = E·eq₁(u_j,t)·H(t), withE = Π_{i<j} eq₁(u_i,s_i)andH(t) = Σ_{x'} eq(u_{>j},x')·h(s_{<j},t,x')a quadratic (the product form of
eq). The card now sums the layer the Gruen way:H(1)andH(2), the factors extended by additions(
2·hi − lo), with noeqfactor in the walk and no program interpreter or slot file. The host formss(1) = E·u_j·H(1), takess(0) = claim − s(1), soE·H(0) = s(0)/(1 − u_j), and extrapolatesH(3) = H(0) + 3·(H(2) − H(1)). Where1 − u_jhas no inverse, the card sumsH(0)too.j's pass first binds the halves tos_{j−1}(reads four cells a factor,writes two) and then sums. No separate fold launch, and one read of each level fewer.
eqtable. The weight iseq(u_{j+1..J−1})[x >> L]·eq(u_{J..})[x mod 2^L]: one small table percard round plus the tail's, all built by one launch a layer. Before, each layer built a
2^mtable (m launches)and folded it every round.
host round over more than a few dozen pairs. The tail gets the factors it got before,
eqincluded, at the smallercube.
gkr_eq_levels_ext3,gkr_round_gruen,gkr_gruen_finish(math-cuda/kernels/sumcheck.cu);host
math_cuda::gkr::GruenLayer(tree layers and the rebuilt input layer),multilinear::gkr_gruen(the knobs,each round's message from the card's sums, a host reference of the whole device algorithm),
gpu::DeviceTree::prove_layer_gruen.★ ARGUE GKR GRUEN: on (the default; LAMBDA_VM_ARGUE_GKR_GRUEN=0 is the old layer rounds; …)once a run;each epoch's
ARGUE GKR #kline ends|| gruen G (xchecked X).Measured on block 25368371 (FAST job 330, one binary at
1946609c3=f3d359998+ the change behind its knob,eight arms A B B A A B B A, wt1402–wt1409; A = the defaults then, B =
LAMBDA_VM_ARGUE_GKR_GRUEN=1, now thedefault). The base and the argue decide; level 1 is reported:
rounds' slot 0.9–1.8 s).
≈ 52 µs a round. Between layers, the host tail fell 657 → 170 ms and the session set-up with the
eqtable.base.
trees 10 → 12.2 a run; device peak 29,266 MiB (A up to 29,298). The host peak read 19.9, 19.7, 16.3 and 20.0 GiB in
the B arms against 16.3 GiB in every A arm. M1-1 allocates nothing on the host; why the peak rose in three arms is
not established (the base now ends ≈ 1.8 s earlier against the same level-1 work).
Soundness: nothing a proof commits to changes.
eqand distributivity move no value, theextrapolation is exact for a quadratic, and
s(0) + s(1) = claimholds for today's own messages whenever a layer isthe fold of the one below, which it is for a tree the card folded. The tail receives today's factor values.
LAMBDA_VM_ARGUE_GKR_GRUEN_XCHECK=1, today's layer program walks the same foldedhalves beside every Gruen round, with its own
eqtable folded on the same challenges; every message and the fivefactors at the crossover are compared, and a difference fails the prove. On the block (job 330's X arm), 3,381 of
3,382 layers compared equal, and the root proved and verified. One layer was not shadowed because the card had no
room for today's
eqtable beside it; it was counted, not skipped silently.stark::multilinear_table::tests::the_argument_proves_the_same_bytes_with_the_gkr_gruen_roundsproves the tall tables with Gruen's rounds (alone, with the other argue knobs, and beside the fused zerocheck) and
compares the canonical bytes table by table and whole, the transcript and the next challenge; it runs on the card in
the gates.
multilinear/tests/argue_gkr_gruen.rs): today's tree against Gruen's rounds at 2^14, 2^16 and2^20 inputs, host tails from cubes of 512, 64, 32 and 2, and with
H(0)summed on the card: 15 proofs equal fieldelement by field element, with the same transcript.
multilinear::gkr_gruen::host_rounds) runs the device algorithm on the host and equalstoday's rounds, challenges and factors at every layer size 2^1–2^9 and every split of card rounds and host tail,
including coordinates of one; three mutations of its arithmetic each fail it.
s(1)) makes the proof differ at the first table and fail GKR'slayer check (
LayerRelationMismatch), and is refused by the cross-check; with the cross-check's comparison madeinert, that test fails.
Gates. FAST job 330 at
1946609c3: the card suite, the host reference, the tall tables' bytes and fault, and themutation. FAST2 job 200 at
7d82a320f: 15 steps, all green (see Gate and CI).Opt-outs.
LAMBDA_VM_ARGUE_GKR_GRUEN=0runs the old layer rounds exactly.LAMBDA_VM_ARGUE_GKR_GRUEN_TAIL=<cube>moves the crossover (a power of two, default 64).
The argue's GKR input layer from the base columns, and no lift (M1-2): same messages, half the tree time
Where the time was. Split per region (
ARGUE REST,ARGUE TREEunderLAMBDA_VM_BASE_SPLIT), the argue's"rest" was mostly the GKR tree region: 1.80–1.98 s a block, of which the card spent 1.42 s writing the input layer
(FAST job 332, each part waiting for its own kernels). Each table lifted its columns into the extension (24 B a cell)
and ran two program launches an interaction over them, ≈ 38 k launches a block, each with its own slot file.
What changed.
constant + Σ coeff·column[row + shift], as base × extension products straight from the epoch's resident columns,from a plan built once a table and kept for the layer's rewrite (
gkr_input_from_columns,logup::input_plan). Thesame cells, so the same tree, output and GKR proof.
reader, and it reads only their base values. The fused kernels now take a row stride (3 for lifted factors, 1 for base
columns) and read the columns where they lie; a public table is a base copy. The
W·rows·24 Blift is made only whenthe old rounds need it: the fused rounds declined (three KECCAK tables at 2^6 rows a block) or the cross-check replays
them. A table with a shifted factor would be lifted as before (none in production).
★ ARGUE GKR INPUT: from the base columns (the default; …)and★ ARGUE NO LIFT: on (the default, …)oncea run; each epoch's
ARGUE TREE #kline ends|| from the columns C · no lift N (late L).Measured on block 25368371 (FAST, one binary each, eight arms A B B A A B B A). The base and the argue decide; level 1
is reported:
87ed8dbcd; A = the defaults then, B =LAMBDA_VM_ARGUE_GKR_INPUT=1): wholeba784bd0b; A = M1-2a, B = +LAMBDA_VM_ARGUE_NO_LIFT=1): wholeM1-2a held; M1-2b's were missed on the beneficial side. It had been sized on the lift's own card time (0.22 s); the
≈ 1.5 GiB the lift held was what the heavy epochs' argues took from the kept WHIR trees, so with it free they stop
evicting them, and the openings stop rebuilding them. Level 1's −0.68 s is not attributed.
Soundness: nothing a proof commits to changes.
over base columns instead of their lifts), and the fused rounds read the same base values through a different stride.
logup::input_layerover the lifted factors for direct and shifted columns, padded andnot (a host test; a mutated shift fails it), and a side reading a public factor has no plan.
multilinear/tests/argue_gkr_input.rs): the columns' tree proves the old tree's proof, output andtranscript at four shapes, carried and handed back (its rewrite); a wrong plan constant moves the output.
stark::multilinear_table::tests::the_argument_proves_the_same_bytes_with_the_input_from_columnsproves the tall tables with the input from the columns alone, beside the production defaults, and with no lift (its
tables reading the columns), against the canonical bytes, transcript and next challenge of the defaults without.
prover::tests::argue_stage1_tests, run alone) pass through the strided kernels, andtest_keccakproves and verifies under the new defaults.Opt-outs.
LAMBDA_VM_ARGUE_GKR_INPUT=0writes the input layer from the lifted factors (and then no lift is offtoo);
LAMBDA_VM_ARGUE_NO_LIFT=0lifts every table's factors.Level 1: the global child proves after the last wide node's artifacts
What changed. In a wide level 1, the WHIR global child's
multi_provenow waits on a card latch until the lastwide node (L1N2 on the block) has built its artifacts.
prologue, its artifacts, its host prep (≈ 1.1 s), then its prove. When the global asked for the card first, L1N2's
artifacts waited out the global's whole prove (0.4–0.9 s), and L1N2's host prep then ran with the card idle.
No arm under 8.0 s had the global first.
then runs during L1N2's host prep, where the card was idle.
multi_provewaits, only on an armed permit, and at most 30 s. After that it queues anyway, counted, with aline saying so.
siblings ≥ tasks); otherwise the lever printsINACTIVEwith the reason, and nothing waits. A level without the global in its pool (wraps,LFM_TREE_TOP_OVERLAP=0, the fixture tree) also makes no latch.★ GLOBAL AFTER LAST: the WHIR GLOBAL child's prove waits until L1N2 has built its artifacts (on by default; LFM_TREE_GLOBAL_AFTER_LAST=0 turns it off),★ GLOBAL AFTER LAST OFF: …, or… requested but INACTIVE: <reason>.CARD DEFER #n multi_prove: waited …s for its latchline for the global.LFM_CARD_TRACE=1, eachCARD HOLD/CARD DEFERline ends· who=<proof>(global, L1N0…, wrap k), sothe card order is read from the log rather than inferred from timing.
Measured on block 25368371 (FAST job 255, one binary at
7d82a320f+ the lever, before M1-2, arms A B B A × 2,wt1520–1527; A = off, B =
LFM_TREE_GLOBAL_AFTER_LAST=1, now the default):standard error (t ≈ −1.2). Both landed inside their pre-registered bands (level 1 [−0.60, −0.10], whole
[−0.60, −0.05]), but this run alone does not separate −0.4 s from a smaller gain.
and B has none. It does not shorten L1N2's prologue (≈ 4.8–5.3 s in both settings), which is now level 1's floor; A's
one arm without the race (7.9 s) is faster than every B arm (8.2–8.6 s).
level 1 −0.19 s and whole −0.12 s with the race gone in every latched arm; its replication (job 253) read whole
−0.04 s. Since then the GKR Gruen rounds shortened the base by ≈ 1.8 s while the wide nodes' prologues start at the
same point (I-GKR's reading), so the global reaches the card first more often and the latch has more to remove: the
global went first in 3 of 4 unlatched arms here, against 4 of 8 in job 252 and 2 of 8 in job 253.
still wins the race at
88b0d3196is unmeasured. Where the race does not happen the latch is already open when theglobal asks, but a race-free arm is not proven free: job 252's latched arms sat 0.05 s above its race-free unlatched
ones, and here A's one race-free arm (7.9 s) beat every latched arm (8.2–8.6 s).
19.7–19.9 GiB (A 2 of 4 arms high, B 3 of 4), so eight arms cannot attribute the +0.9 GiB to the latch.
Soundness: nothing a proof commits to changes. The latch moves one card request in time. The five program ids were
identical in all eight arms of job 255, and every root verified at 180 words. The gates below prove the production tree
at the default, under
=0and with too few workers, and diff each tree's five ids against job 255's (= #1010's).Opt-out.
LFM_TREE_GLOBAL_AFTER_LAST=0restores first come, first served. Any value other than unset,0or1stops the run.
WHIR grinding at 18 bits, 114 queries
What changed. Every WHIR chain, in the base and in every recursion proof, now grinds 18 bits before its query
positions instead of 20, and opens 114 queries instead of 112 to buy the two bits back. It is one setting,
multilinear_prove::chain_config_under, behind the knobLAMBDA_VM_ZF_WHIR_GRIND_BITS=20|18(default 18). Commits:fc0ff59 (the knob), 329b9c6 (an ignored per-height census of the chain verifier at 20 and 18), 5364aa2 (the
default flip), 2687e48 (the W-leg sizing test pins follow the process's bits).
Measured (FAST, one binary, eight arms A B B A A B B A, wt1660–1667; A =
=20, B = 18):The grind work fell 2.3× rather than the 4× that two fewer bits alone would give: each grind keeps a fixed launch and
readback cost.
Soundness: no proven bits are lost.
phase moves from 130.926 to 130.907 bits.
security/zisk_calc.py).setting does not verify at the other.
padded to 2^18, with 3,542 rows (1.35 %) of headroom.
crypto suites; the production tree at 18 bits (banner 18, q = 114) and at
=20, each matching its reference programids; the stricter-verifier refusal, the legacy-bytes known-answer test, and every chain test, ignored ones included.
Opt-out.
LAMBDA_VM_ZF_WHIR_GRIND_BITS=20restores 20 bits and 112 queries, and the program ids of the branchbefore this change.
What is in the branch
for the block.
(−8.3 s).
inside level 0's pool, saved −11.9 s. Together they took the block to 128.3 s.
ZfFormat(prover/src/zf_format.rs) parses sevenLAMBDA_VM_ZF_*knobs once and prints oneZF FORMAT:banner. The default iscap=auto whir_cap=auto fri=dp one_row=0 whir_folds=first6 whir_stack=27 whir_grind=query.end of each tree's first path, so the proof structs are unchanged.
chain.
8–11 of 2^25.
whir_grind, defaultquery: one grind and one nonce a round inthe WHIR chains; see "Grinding only before the queries" above.
LAMBDA_VM_ZF_ONE_ROW=auto) are built on host, on the GPU andin-guest, but are off here: they cost +3.2 s on this pipeline. They are on in the STARK pipeline's PR (STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s #1009).
ZfFormat::LEGACYstays pinned by a golden test. The RV64 recursion guestverifies only the legacy format.
crypto/math-cuda/src/lde_cm.rs,kernels/ntt_cm.cu).zero fill, and a transpose before a row-major commit.
launch in registers and shared memory, so a 2^22 transform is three passes. The coset spread is fused into the
first pass, and the output is column-major, so the commits lose their transpose.
commit's encoding. LDEs that keep a host copy (below 2^19 rows) stay on the old path.
LAMBDA_VM_LDE_LEGACY=1sends every LDE back to the per-level pipeline.gap-fix/ntt(da2da9d93),gap-fix/wbatch-int(7e3eac501),gap-fix/harness(f81f0a80f),gap-fix/rec-int(c679a771b),gap-fix/stack-int(8c2450ff6) andgap-fix/idle-a-int(d3c76d2ed), eacha signed merge;
gap-fix/idle-b-int(bdb2d37b6) andgap-fix/hash-int(e041e9fb0), each a signed merge;gap-fix/kern-int, one commit (d1dc45514).the stack.
9cea599a3(the nonce layout, default off),ce292de3e(the default)and
b4506b719(comments).93a2b5643(behind its knob), merged asc7228f310, and8930490e5(the default).34c17603b, merged as7364d1292, andb9698b05d(thedefault).
whir/full-recursion(4150afab6), merged as3722e7376;70cdb3719(its pins under P2-W)and
6a6e26611(the default).1177d5a13(the census) and965e13de2(behind its knob), merged as06d2d48e8;26adbf501(the default) anda28ad36af(the W-LFM parity tests). The merge also carries two argue knobswhose A/Bs read MECHANISM-ONLY,
LAMBDA_VM_ARGUE_LEAN_READSandLAMBDA_VM_ARGUE_LEAN_TAIL, both off.d61a3c729) and deterministic whir_chain grind tests (d6648e653, merged as5f15641b9).1e3c39d5e(a device-entry counter),533a22926(behind itsknob),
78781f7cf(the default) and4ab853c6c(the pure-WHIR tree's default fan-in 4).529589d9d(a tree of one wide level runs root option A as option B) and61b025b7d(a spin guest anda test that proves 1 to 6 epochs to a verified root). A block of 2 to fan-in epochs used to stop at the root's
child-count check; block 25368371's tree is unchanged.
e783f29d5(the WHIR driver takes fan-in 5 fromLFM_CENSUS_FAN_IN) andb682091a3(the default).d117ffedd(behind its knob) andeb20fe04f(the default). The GKR tree'srefusals counted:
fd3146a0b(the fan-in-5 margin quoted in MiB),7650b53c7(the counter),a28690b7f(itsforced-refusal test) and
4593752a7(the test's feature note). Merged as33232d688.deb9726b3, reverted by9e2728955(whose tree equals33232d688's). Its A/B read −0.50 s (job 244), but at the landed head it measured no effect: 40.30 s with theclaim and 40.30 s without (job 245). Level 1 gained ≈ 0.2 s and the base paid it back.
63ba2baf0(behind its knob),b8148e4fe(its card test),bb7f5d8ee(the count on the retention line) and73342bc66(the default).LFM_WHIR_KEEP_FUTILE=0opts out.3332c1bf3(behind its knob),f891296de(its card byte-identity test),22b81fc63(the served openings on the retention line),c68d37f16(the default, and the comments that said a treeis never kept) and
7c8272701(the retention card tests in both modes, and H4's memory guard restated as "nothingof a tree outside its promise").
LFM_WHIR_WHOLE_TREES=0opts out.45fb0774f(the evictor passes over a tree an openingreads; its card test and two mutations).
53d52af9c(the host referencemultilinear::fused, parity on every table, atest-only capture hook),
a14f35b8a(the card rounds, behind their knobs),1a07ce50dand6b80511f8(the cardtests run alone, each table at a height the card uploads),
6ba799072(the tables named on their log lines),4e40b5d09(a table without roots launches no grid pass: the crash the first timing found),5cbbb683f(bothdefaults on, their banners and the split's fused row) and
f3d359998(the canonical-bytes test and the fused faultin stark; the faults per thread).
LAMBDA_VM_ARGUE_FUSED=0andLAMBDA_VM_ARGUE_INT_NODES=0opt out.1946609c3(the kernels,GruenLayer,gkr_gruenwith itshost reference, the cross-check, the card and tall-table tests, behind the knob) and
7d82a320f(the default, pinnedby a unit test).
LAMBDA_VM_ARGUE_GKR_GRUEN=0opts out.6623da0cb(ARGUE RESTper epoch,ARGUE AIRper table, underLAMBDA_VM_BASE_SPLIT),35265830fandfff43adf3(ARGUE TREE, andLAMBDA_VM_ARGUE_TREE_SYNC, a diagnostic).87ed8dbcd(the kernel, the plan, thecolumns' tree, its card and tall-table tests, behind the knob),
ba784bd0b(no lift: the strided fused kernels,ColumnFactors, the late lift, behind its knob) andd108cabb5(both defaults, pinned by unit tests).LAMBDA_VM_ARGUE_GKR_INPUT=0andLAMBDA_VM_ARGUE_NO_LIFT=0opt out.395829a79(the latch, the deferral and the opener indevice_permit, behindLFM_TREE_GLOBAL_AFTER_LAST),3d20815a2(each card hold's proof named on its trace line),efdb528d7(thelever's mode: no global in the pool, too few workers, small blocks) and
88b0d3196(the default, pinned by a unittest).
LFM_TREE_GLOBAL_AFTER_LAST=0opts out.main: perf(alloc): compile jemalloc's never-purge policy into the binary #996 (jemalloc never-purge compiled into the CLI).Soundness
Query counts and blowup are unchanged.
The format levers
cap node the query index selects. Path lengths are checked exactly, including at c = 0.
changes, in a term that stays more than 50 bits below the dominant one.
layout Plonky3 uses. The query index is uniform over the whole domain.
fewer rounds, and queries stay 112 per round.
The gap fixes
all take the layout from
global_layout(shapes, cap), never from a proof.table. It stays 112 at every production shape.
security/zisk_calc.py): the WHIRchain minimum is 130.393 bits at 27, against 130.926 at 25. With the per-table STARK recursion
(
LAMBDA_VM_LFM_PROVER=stark) the pipeline minimum is 128.946 bits, set by the query phase of every LFM proof; withthe default pure WHIR recursion it is 130.393 bits (see "Pure WHIR recursion").
message, so a cheating prover can re-draw α₁ by varying h₁ without grinding again. The bits above are the unground
ones. P2-W drops the folding and out-of-domain grinds (see "Grinding only before the queries"); K4 changes only how
the card searches for the nonce.
sender, its honest multiplicities are all zero and the table constrains nothing.
instantiated chip's interactions, stored in the artifacts and folded into
program_id, and the verifier re-checksit against the mask it was handed. No proof supplies it.
LAMBDA_VM_LFM_KEEP_BITWISE=1reproduces the legacy registry digests.emissions compute the same field value on accepted and on tampered chains (tests). The WHIR wrap program ids move.
program_idand never read from aproof. Tests refuse a forged tail root, the single-table door and a wrong chunk root.
parity through either staging, on the card;
reference, and the fault suite under both settings;
leaf layer, reads a kept tree or hashes the leaves again; the same tree, root and paths, by card tests that compare
against a fresh codeword both ways, and the program ids of every A/B arm and gate tree;
identity), by the cross-check arm on the block (390 of 390 tables' messages equal to today's), by the tall tables'
canonical proof bytes on the card, and by the program ids of every A/B arm and gate tree;
block (3,381 of 3,382 layers compared equal, one not shadowed for room), by the tall tables' canonical bytes on the
card, and by the program ids of every A/B arm and gate tree;
the plan's host test against the lifted layer, the card tree tests, the tall tables' canonical bytes on the card
(with and without the lift), and the program ids of every A/B arm and gate tree;
and gate tree.
the 64-bit multiply. Its bytes were shown equal three ways:
with a failing control). It also replays the cooperative kernels lane by lane (the half-warp Merkle kernels and
the queue grind) against the shipped ones. CI runs it on every PR;
path and, where cheap, against the host oracle (
rpx_device_paths);Fixed along the way
tables, which rejected honest proofs that publish values.
failed, the error was dropped, and every such commit fell back to the host; the base took 647 s. The grid now splits
into z, and device commit and tree errors are logged and counted.
source codeword dropped.
GPU.
Gate and CI
M1-2 and the level-1 latch were gated together, in one run at this head (
88b0d3196), FAST job 401: GATES GREEN, 18 of 18 steps (guest267/267; math-cuda 279 passed, 16 ignored; RPX device parity 11; stark 423 passed, 6 ignored; crypto 164; the 12
landing lines below; the prover's lib suite 1,650 passed, 100 ignored). Its latch lines: the latch's 14 unit tests (the default and the opt-out, the mode and the deadlock
guard, the latch, the deferral, the opener on unwind, the holder names); the production tree at the defaults (the
latch's banner, exactly one
CARD DEFER, the global's, inside its bound, the global's prove after L1N2's artifacts),under
LFM_TREE_GLOBAL_AFTER_LAST=0(the off banner, noCARD DEFER) and with three workers for level 1's four tasks(the guard's INACTIVE line, no
CARD DEFER), each with #1010's 5 program ids; and the six small blocks (the fixturetree's no-global INACTIVE line six times, no
CARD DEFER, every root verified). The same latch lines ran green onthe latch alone at
3a9015138(7d82a320f+ the latch), FAST job 400. Its M1-2 lines: on the host, the knob pins,the plan and the split lines (59); on the card,
--test argue_gkr_input(2) and--test argue_gkr_gruen(4), stark'smultilinear_tablemodule (the canonical-bytestests, the no-lift arm reading the columns), and the six fused card tests through the strided kernels; the production
tree at the defaults (≥ 200 trees from the columns, ≥ 200 tables with no lift), under
LAMBDA_VM_ARGUE_NO_LIFT=0andunder
LAMBDA_VM_ARGUE_GKR_INPUT=0, each with #1010's 5 program ids. Before it, each half's device gates ran green inits A/B job (FAST 333 and 335).
M1-1 was gated at
7d82a320f, on the FAST2 box (job 200): 15 steps, all green — guest artifacts 267 / 267,math-cuda 279 / 0 / 16, RPX device parity 11, stark 422 / 0 / 6, crypto 164, the lib suite 1,640 / 0 / 100. Besides the
standard steps:
multilinear --lib gkr whir_split(48: the host reference, the default pinned, the split lines);--test argue_gkr_gruen(4) and--test argue_lean_tail(3) under the new default,-p stark --features cuda,multilinear/cuda --lib multilinear_table(35, the canonical-bytes and fault tests amongthem) and
-p multilinear --features cuda --lib(374);LAMBDA_VM_ARGUE_GKR_GRUEN=0(0 Gruen layers on every epoch, the opt-out's banner, the same ids), and at thedefault with the cross-check (3,381 of 3,382 layers compared equal, the same ids), each root verified.
Stage 1 of the argue was gated at
f3d359998, on the FAST2 box: 16 steps, all green (the lib suite1,640 / 0 / 100). Besides the standard steps: the defaults pinned on the host; on the card, the fused rounds against
today's host rounds (42 runs), the twelve tables without roots under the production switches,
test_keccakproved andverified with and without the cross-check, and the integer-node rounds; both negative controls with their mutations
red; real traces under the cross-check, none parted;
-p multilinear --features cuda --liband-p stark --features cuda,multilinear/cuda --lib multilinear_table(the canonical-bytes test on the card among them); and the productiontree at the defaults (298 fused sessions, 947 openings served, #1010's 5 program ids) and under both opt-outs (no fused
session, the same ids).
The kept tree's promise by its last handle was gated at
45fb0774f, on the FAST2 box: 13 steps, all green (the libsuite 1,634 / 0 / 96), with its card test, both mutations failing it, the retention files under
LFM_WHIR_WHOLE_TREES=0, and the production tree at the default (952 openings served, 0 passed over, #1010's 5program ids).
Whole trees were gated at
7c8272701, on the FAST2 box: 14 steps, all green (the lib suite 1,634 / 0 / 96).Besides the standard steps: the retention unit tests with the default pinned; on the card, a kept whole tree serving
its openings byte-equal to the leaf-layer reference, and the futile miss at the new default; the tree-cache file at the
default and under
LFM_WHIR_WHOLE_TREES=0(H4's group guard in both modes: pool share 0 MiB, the ledger exact); andthe production tree at the default (952 openings served, #1010's 5 program ids) and under the opt-out (0 served,
the same ids).
Keeping the leaf layers through a futile miss was gated at
73342bc66, on the FAST2 box: 12 steps, all green (the libsuite 1,634 / 0 / 96), with the card test both ways and the production tree at the default and under
LFM_WHIR_KEEP_FUTILE=0, each with #1010's 5 program ids.The head ahead and the refusal counter were gated at
33232d688, on the FAST2 box: 14 steps, all green(the lib suite 1,634 / 0 / 96). Besides the standard steps:
LAMBDA_VM_WHIR_HEAD_AHEAD=0, each with the fan-in-5 landing's 5program ids;
A supplementary gate ran the per-table argument's suite on the card, 5 steps, all green. An audit found that the
suite's earlier gate line (
-p stark --features cuda) ran multilinear's host paths only: stark'scudadoes notturn on
multilinear/cuda. The supplement names both features and requires every device arm's own output line.Fan-in 5 was gated at
b682091a3, on the FAST2 box: 15 steps, all green (the lib suite 1,631 / 0 / 96).Besides the standard steps: the root, tree-shape and knob suites; 1 to 6 epochs proved to a verified root at the
default (fan-in 5), under
LAMBDA_VM_LFM_WIDE=offand understark; the fixture tree to a block artifact; and theproduction tree four times, at the default (its 5 program ids), under
LFM_CENSUS_FAN_IN=4(4ab853c6c's 6), underLFM_CENSUS_FAN_IN=3(5f15641b9's 9) and underLAMBDA_VM_LFM_PROVER=stark(the STARK recursion's 24).Small blocks was gated at
61b025b7d, on the FAST2 box: 12 steps, all green (the lib suite 1,631 / 0 / 96),including 1 to 6 epochs proved to a verified root at the default, under
LAMBDA_VM_LFM_WIDE=offand understark, andthe production tree's 6 program ids unchanged.
The permit after the prep and fan-in 4 were gated at
4ab853c6c, on the FAST2 box: 14 steps, all green (thelib suite 1,628 / 0 / 95). Besides the standard steps: the permit's byte gate and device-entry gate, the fixture tree at
the new defaults and under
LFM_CARD_AFTER_PREP=0, and the production tree three times, at the defaults (its 6 programids), under
LFM_CENSUS_FAN_IN=3(5f15641b9's 9) and underLAMBDA_VM_LFM_PROVER=stark(the STARK recursion's 24).N1′, the MDS fix and the grind tests were gated at
5f15641b9, on the FAST2 box: 21 steps, all green (thelib suite 1,625 / 0 / 94): the standard six, N1′'s 13 (card parity on the five big batches, the whole argument's
identity and its negative control, the slot-budget pin, multilinear's lib at the default and under the opt-out, and the
byte gate for both hashes and under the opt-out) and the MDS fix's 2 (the RPX suites).
Pure WHIR was gated at
6a6e26611, on the FAST2 box: 14 steps, all green (the lib suite 1,622 / 0 / 92). These are the standard steps,plus the WHIR recursion's prover, verifier, leg, wide-node, switch and lead-in suites on the card with their negative
tests, the fixture tree at the default and under the opt-out, and the opt-out's byte gate: the production tree under
LAMBDA_VM_LFM_PROVER=starkprints8930490e5's 24 program ids.A2+A3 was gated at
b9698b05don FAST2: 17 steps, all green.A1 was gated at
8930490e5, on the FAST2 box (the second RTX 5090): 14 steps, all green. These are thestandard steps, plus A1's device tests, the whole argument's identity and its negative control, the multilinear suite at
the new default and under the opt-out, and the WHIR byte gate on both hashes and under the opt-out.
P2-W was gated at
b4506b719on the FAST box: 11 steps, all green. These are the standard steps, plus themultilinear suite, the WHIR chain gates with their production-shape emissions, the WHIR byte gate on both hashes, and
the WHIR epoch verifier programs under the opt-out.
The batch was gated at
d1dc45514on the FAST box: 81 steps, every one at its exact pre-registered count.The standard steps:
The 75 targeted lines cover:
the room on the card;
tests;
For each switch of the last two rounds, a gate line runs each setting and reads the banner its process printed. The
previous candidate without K6 (
41549ebad) passed its own 70-step gate. The cumulative ABBA in the first table ranafter the gate.
In CI at
d1dc45514, these pass: lint, the host known-answer tests (including the RPX lane-by-lane replay), the provertest build, the stark cuda-feature tests, and the CLI and executor tests. The spec structure check fails on a key the
spec tooling does not know (
spec/src/blake3.toml:constants). The prover shards were still running when this waswritten.
Open decisions
b4506b719). Since then this PR added the WHIR-sidefixes (A1, A2+A3, pure WHIR, N1′, the permit after the prep, small blocks, fan-in 5) and STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s #1009 the STARK-side ones
(R1b, F-SIDLE, NICE v2); both carry the MDS fix. The shared defaults differ in the recursion prover (WHIR here, STARK
in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s #1009),
one_row(off here, auto in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s #1009) and the LFM_HASH split (off here, on in STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s #1009). A per-pipeline defaultwould let one PR carry both.
LAMBDA_VM_MEMPOOL_RELEASE_MB=0, which releases thedevice memory pool; the code's default retains it. Retaining measured −4.50 s on this pipeline before the engine, but
only −0.45 s at the current head (inside noise), so this PR keeps reporting with the release. The STARK PR (STARK recursion on GPU (RPX) with ZisK-style proof formats: block 25368371 in 60.18 s #1009)
measured −2.00 s and reports with the retain.
budget at 27. A block that adds one polynomial to such an epoch moves that argument's reservation to the host:
counted, proof unchanged, slower. The device peak before no lift was 29,266 MiB (the highest of an A/B's eight
arms) of the card's 32,607 MiB. Worth a run on a heavier block before relying on 27 there.
With whole trees kept, the base's heaviest argues run at the budget, and stage 1's zerocheck adds 523 MiB there: the
argue takes kept trees back (10 a run, where 2 before) and pays their rebuilds. Everything kept is evictable, so a
heavier block pays the old rebuilds first and falls back only where it fell back before; the same run would check
it. M1-1 reserves nothing new and drops the layer-sized
eqtable its sessions allocated; its A/B left the argue'sreserved peak unchanged (25,660 MiB) with 12.2 kept trees evicted a run against 10. M1-2's no lift then frees the
lift's room: the argue's reserved peak is 24,153 MiB, below the budget, and 2.2 kept trees are evicted a run.
keeps 128 bits.
iteration.